Step | Hyp | Ref
| Expression |
1 | | ssun2 3777 |
. . . 4
⊢ 𝑌 ⊆ ({𝐵} ∪ 𝑌) |
2 | | reldom 7961 |
. . . . . 6
⊢ Rel
≼ |
3 | 2 | brrelex2i 5159 |
. . . . 5
⊢ (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → ({𝐵} ∪ 𝑌) ∈ V) |
4 | 3 | adantl 482 |
. . . 4
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → ({𝐵} ∪ 𝑌) ∈ V) |
5 | | ssexg 4804 |
. . . 4
⊢ ((𝑌 ⊆ ({𝐵} ∪ 𝑌) ∧ ({𝐵} ∪ 𝑌) ∈ V) → 𝑌 ∈ V) |
6 | 1, 4, 5 | sylancr 695 |
. . 3
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → 𝑌 ∈ V) |
7 | | brdomi 7966 |
. . . . 5
⊢ (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → ∃𝑓 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌)) |
8 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
9 | 8 | resex 5443 |
. . . . . . . . . 10
⊢ (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∈ V |
10 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌)) |
11 | | difss 3737 |
. . . . . . . . . . 11
⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) ⊆ ({𝐴} ∪ 𝑋) |
12 | | f1ores 6151 |
. . . . . . . . . . 11
⊢ ((𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) ∧ (({𝐴} ∪ 𝑋) ∖ {𝐴}) ⊆ ({𝐴} ∪ 𝑋)) → (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) |
13 | 10, 11, 12 | sylancl 694 |
. . . . . . . . . 10
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) |
14 | | f1oen3g 7971 |
. . . . . . . . . 10
⊢ (((𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∈ V ∧ (𝑓 ↾ (({𝐴} ∪ 𝑋) ∖ {𝐴})):(({𝐴} ∪ 𝑋) ∖ {𝐴})–1-1-onto→(𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) |
15 | 9, 13, 14 | sylancr 695 |
. . . . . . . . 9
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴}))) |
16 | | df-f1 5893 |
. . . . . . . . . . . . 13
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) ↔ (𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) ∧ Fun ◡𝑓)) |
17 | 16 | simprbi 480 |
. . . . . . . . . . . 12
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → Fun ◡𝑓) |
18 | | imadif 5973 |
. . . . . . . . . . . 12
⊢ (Fun
◡𝑓 → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴}))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴}))) |
20 | 19 | ad2antll 765 |
. . . . . . . . . 10
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) = ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴}))) |
21 | | snex 4908 |
. . . . . . . . . . . . . 14
⊢ {𝐵} ∈ V |
22 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑌 ∈ V) |
23 | | unexg 6959 |
. . . . . . . . . . . . . 14
⊢ (({𝐵} ∈ V ∧ 𝑌 ∈ V) → ({𝐵} ∪ 𝑌) ∈ V) |
24 | 21, 22, 23 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ({𝐵} ∪ 𝑌) ∈ V) |
25 | | difexg 4808 |
. . . . . . . . . . . . 13
⊢ (({𝐵} ∪ 𝑌) ∈ V → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V) |
27 | | f1f 6101 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌)) |
28 | | imassrn 5477 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ran 𝑓 |
29 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) → ran 𝑓 ⊆ ({𝐵} ∪ 𝑌)) |
30 | 28, 29 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌)) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌)) |
32 | 31 | ad2antll 765 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ ({𝐴} ∪ 𝑋)) ⊆ ({𝐵} ∪ 𝑌)) |
33 | 32 | ssdifd 3746 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ (𝑓 “ {𝐴}))) |
34 | | f1fn 6102 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑓 Fn ({𝐴} ∪ 𝑋)) |
35 | 34 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑓 Fn ({𝐴} ∪ 𝑋)) |
36 | | domunsncan.a |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 ∈ V |
37 | 36 | snid 4208 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 ∈ {𝐴} |
38 | | elun1 3780 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ ({𝐴} ∪ 𝑋)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ∈ ({𝐴} ∪ 𝑋) |
40 | | fnsnfv 6258 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn ({𝐴} ∪ 𝑋) ∧ 𝐴 ∈ ({𝐴} ∪ 𝑋)) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
41 | 35, 39, 40 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → {(𝑓‘𝐴)} = (𝑓 “ {𝐴})) |
42 | 41 | difeq2d 3728 |
. . . . . . . . . . . . 13
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) = (({𝐵} ∪ 𝑌) ∖ (𝑓 “ {𝐴}))) |
43 | 33, 42 | sseqtr4d 3642 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)})) |
44 | | ssdomg 8001 |
. . . . . . . . . . . 12
⊢ ((({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∈ V → (((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ⊆ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}))) |
45 | 26, 43, 44 | sylc 65 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)})) |
46 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:({𝐴} ∪ 𝑋)⟶({𝐵} ∪ 𝑌) ∧ 𝐴 ∈ ({𝐴} ∪ 𝑋)) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌)) |
47 | 27, 39, 46 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌)) |
48 | 47 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌)) |
49 | | domunsncan.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
50 | 49 | snid 4208 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ {𝐵} |
51 | | elun1 3780 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ ({𝐵} ∪ 𝑌)) |
52 | 50, 51 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝐵 ∈ ({𝐵} ∪ 𝑌)) |
53 | | difsnen 8042 |
. . . . . . . . . . . 12
⊢ ((({𝐵} ∪ 𝑌) ∈ V ∧ (𝑓‘𝐴) ∈ ({𝐵} ∪ 𝑌) ∧ 𝐵 ∈ ({𝐵} ∪ 𝑌)) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
54 | 24, 48, 52, 53 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
55 | | domentr 8015 |
. . . . . . . . . . 11
⊢ ((((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ∧ (({𝐵} ∪ 𝑌) ∖ {(𝑓‘𝐴)}) ≈ (({𝐵} ∪ 𝑌) ∖ {𝐵})) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
56 | 45, 54, 55 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → ((𝑓 “ ({𝐴} ∪ 𝑋)) ∖ (𝑓 “ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
57 | 20, 56 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
58 | | endomtr 8014 |
. . . . . . . . 9
⊢
(((({𝐴} ∪ 𝑋) ∖ {𝐴}) ≈ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ∧ (𝑓 “ (({𝐴} ∪ 𝑋) ∖ {𝐴})) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
59 | 15, 57, 58 | syl2anc 693 |
. . . . . . . 8
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) ≼ (({𝐵} ∪ 𝑌) ∖ {𝐵})) |
60 | | uncom 3757 |
. . . . . . . . . . . 12
⊢ ({𝐴} ∪ 𝑋) = (𝑋 ∪ {𝐴}) |
61 | 60 | difeq1i 3724 |
. . . . . . . . . . 11
⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) = ((𝑋 ∪ {𝐴}) ∖ {𝐴}) |
62 | | difun2 4048 |
. . . . . . . . . . 11
⊢ ((𝑋 ∪ {𝐴}) ∖ {𝐴}) = (𝑋 ∖ {𝐴}) |
63 | 61, 62 | eqtri 2644 |
. . . . . . . . . 10
⊢ (({𝐴} ∪ 𝑋) ∖ {𝐴}) = (𝑋 ∖ {𝐴}) |
64 | | difsn 4328 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ 𝑋 → (𝑋 ∖ {𝐴}) = 𝑋) |
65 | 63, 64 | syl5eq 2668 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ 𝑋 → (({𝐴} ∪ 𝑋) ∖ {𝐴}) = 𝑋) |
66 | 65 | ad2antrr 762 |
. . . . . . . 8
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐴} ∪ 𝑋) ∖ {𝐴}) = 𝑋) |
67 | | uncom 3757 |
. . . . . . . . . . . 12
⊢ ({𝐵} ∪ 𝑌) = (𝑌 ∪ {𝐵}) |
68 | 67 | difeq1i 3724 |
. . . . . . . . . . 11
⊢ (({𝐵} ∪ 𝑌) ∖ {𝐵}) = ((𝑌 ∪ {𝐵}) ∖ {𝐵}) |
69 | | difun2 4048 |
. . . . . . . . . . 11
⊢ ((𝑌 ∪ {𝐵}) ∖ {𝐵}) = (𝑌 ∖ {𝐵}) |
70 | 68, 69 | eqtri 2644 |
. . . . . . . . . 10
⊢ (({𝐵} ∪ 𝑌) ∖ {𝐵}) = (𝑌 ∖ {𝐵}) |
71 | | difsn 4328 |
. . . . . . . . . 10
⊢ (¬
𝐵 ∈ 𝑌 → (𝑌 ∖ {𝐵}) = 𝑌) |
72 | 70, 71 | syl5eq 2668 |
. . . . . . . . 9
⊢ (¬
𝐵 ∈ 𝑌 → (({𝐵} ∪ 𝑌) ∖ {𝐵}) = 𝑌) |
73 | 72 | ad2antlr 763 |
. . . . . . . 8
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → (({𝐵} ∪ 𝑌) ∖ {𝐵}) = 𝑌) |
74 | 59, 66, 73 | 3brtr3d 4684 |
. . . . . . 7
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ (𝑌 ∈ V ∧ 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌))) → 𝑋 ≼ 𝑌) |
75 | 74 | expr 643 |
. . . . . 6
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌)) |
76 | 75 | exlimdv 1861 |
. . . . 5
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (∃𝑓 𝑓:({𝐴} ∪ 𝑋)–1-1→({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌)) |
77 | 7, 76 | syl5 34 |
. . . 4
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑌 ∈ V) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) → 𝑋 ≼ 𝑌)) |
78 | 77 | impancom 456 |
. . 3
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → (𝑌 ∈ V → 𝑋 ≼ 𝑌)) |
79 | 6, 78 | mpd 15 |
. 2
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) → 𝑋 ≼ 𝑌) |
80 | | en2sn 8037 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴} ≈ {𝐵}) |
81 | 36, 49, 80 | mp2an 708 |
. . . 4
⊢ {𝐴} ≈ {𝐵} |
82 | | endom 7982 |
. . . 4
⊢ ({𝐴} ≈ {𝐵} → {𝐴} ≼ {𝐵}) |
83 | 81, 82 | mp1i 13 |
. . 3
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → {𝐴} ≼ {𝐵}) |
84 | | simpr 477 |
. . 3
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → 𝑋 ≼ 𝑌) |
85 | | incom 3805 |
. . . . 5
⊢ ({𝐵} ∩ 𝑌) = (𝑌 ∩ {𝐵}) |
86 | | disjsn 4246 |
. . . . . 6
⊢ ((𝑌 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝑌) |
87 | 86 | biimpri 218 |
. . . . 5
⊢ (¬
𝐵 ∈ 𝑌 → (𝑌 ∩ {𝐵}) = ∅) |
88 | 85, 87 | syl5eq 2668 |
. . . 4
⊢ (¬
𝐵 ∈ 𝑌 → ({𝐵} ∩ 𝑌) = ∅) |
89 | 88 | ad2antlr 763 |
. . 3
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → ({𝐵} ∩ 𝑌) = ∅) |
90 | | undom 8048 |
. . 3
⊢ ((({𝐴} ≼ {𝐵} ∧ 𝑋 ≼ 𝑌) ∧ ({𝐵} ∩ 𝑌) = ∅) → ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) |
91 | 83, 84, 89, 90 | syl21anc 1325 |
. 2
⊢ (((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) ∧ 𝑋 ≼ 𝑌) → ({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌)) |
92 | 79, 91 | impbida 877 |
1
⊢ ((¬
𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) ↔ 𝑋 ≼ 𝑌)) |