Step | Hyp | Ref
| Expression |
1 | | refrel 22405 |
. . . . . . 7
⊢ Rel
Ref |
2 | 1 | brrelex2i 5606 |
. . . . . 6
⊢ (𝐵Ref𝐴 → 𝐴 ∈ V) |
3 | 2 | adantl 485 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝐴 ∈ V) |
4 | 1 | brrelex1i 5605 |
. . . . . 6
⊢ (𝐵Ref𝐴 → 𝐵 ∈ V) |
5 | 4 | adantl 485 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝐵 ∈ V) |
6 | | unexg 7534 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V) |
7 | 3, 5, 6 | syl2anc 587 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝐴 ∪ 𝐵) ∈ V) |
8 | | ssun2 4087 |
. . . . . 6
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝐵 ⊆ (𝐴 ∪ 𝐵)) |
10 | | ssun1 4086 |
. . . . . . 7
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝐴 ⊆ (𝐴 ∪ 𝐵)) |
12 | | eqimss2 3958 |
. . . . . . . . 9
⊢ (𝑋 = 𝑌 → 𝑌 ⊆ 𝑋) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝑌 ⊆ 𝑋) |
14 | | ssequn2 4097 |
. . . . . . . 8
⊢ (𝑌 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑌) = 𝑋) |
15 | 13, 14 | sylib 221 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝑋 ∪ 𝑌) = 𝑋) |
16 | 15 | eqcomd 2743 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝑋 = (𝑋 ∪ 𝑌)) |
17 | | refssfne.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐴 |
18 | | refssfne.2 |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐵 |
19 | 17, 18 | uneq12i 4075 |
. . . . . . . 8
⊢ (𝑋 ∪ 𝑌) = (∪ 𝐴 ∪ ∪ 𝐵) |
20 | | uniun 4844 |
. . . . . . . 8
⊢ ∪ (𝐴
∪ 𝐵) = (∪ 𝐴
∪ ∪ 𝐵) |
21 | 19, 20 | eqtr4i 2768 |
. . . . . . 7
⊢ (𝑋 ∪ 𝑌) = ∪ (𝐴 ∪ 𝐵) |
22 | 17, 21 | fness 34275 |
. . . . . 6
⊢ (((𝐴 ∪ 𝐵) ∈ V ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ 𝑋 = (𝑋 ∪ 𝑌)) → 𝐴Fne(𝐴 ∪ 𝐵)) |
23 | 7, 11, 16, 22 | syl3anc 1373 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → 𝐴Fne(𝐴 ∪ 𝐵)) |
24 | | elun 4063 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
25 | | ssid 3923 |
. . . . . . . . . . 11
⊢ 𝑥 ⊆ 𝑥 |
26 | | sseq2 3927 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑥)) |
27 | 26 | rspcev 3537 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑥) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
28 | 25, 27 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
29 | 28 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
30 | | refssex 22408 |
. . . . . . . . . . 11
⊢ ((𝐵Ref𝐴 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
31 | 30 | ex 416 |
. . . . . . . . . 10
⊢ (𝐵Ref𝐴 → (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
32 | 31 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
33 | 29, 32 | jaod 859 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
34 | 24, 33 | syl5bi 245 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝑥 ∈ (𝐴 ∪ 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
35 | 34 | ralrimiv 3104 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
36 | 21, 17 | isref 22406 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ∈ V → ((𝐴 ∪ 𝐵)Ref𝐴 ↔ (𝑋 = (𝑋 ∪ 𝑌) ∧ ∀𝑥 ∈ (𝐴 ∪ 𝐵)∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
37 | 7, 36 | syl 17 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → ((𝐴 ∪ 𝐵)Ref𝐴 ↔ (𝑋 = (𝑋 ∪ 𝑌) ∧ ∀𝑥 ∈ (𝐴 ∪ 𝐵)∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
38 | 16, 35, 37 | mpbir2and 713 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝐴 ∪ 𝐵)Ref𝐴) |
39 | 9, 23, 38 | jca32 519 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → (𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴Fne(𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵)Ref𝐴))) |
40 | | sseq2 3927 |
. . . . . 6
⊢ (𝑐 = (𝐴 ∪ 𝐵) → (𝐵 ⊆ 𝑐 ↔ 𝐵 ⊆ (𝐴 ∪ 𝐵))) |
41 | | breq2 5057 |
. . . . . . 7
⊢ (𝑐 = (𝐴 ∪ 𝐵) → (𝐴Fne𝑐 ↔ 𝐴Fne(𝐴 ∪ 𝐵))) |
42 | | breq1 5056 |
. . . . . . 7
⊢ (𝑐 = (𝐴 ∪ 𝐵) → (𝑐Ref𝐴 ↔ (𝐴 ∪ 𝐵)Ref𝐴)) |
43 | 41, 42 | anbi12d 634 |
. . . . . 6
⊢ (𝑐 = (𝐴 ∪ 𝐵) → ((𝐴Fne𝑐 ∧ 𝑐Ref𝐴) ↔ (𝐴Fne(𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵)Ref𝐴))) |
44 | 40, 43 | anbi12d 634 |
. . . . 5
⊢ (𝑐 = (𝐴 ∪ 𝐵) → ((𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) ↔ (𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴Fne(𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵)Ref𝐴)))) |
45 | 44 | spcegv 3512 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ∈ V → ((𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴Fne(𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵)Ref𝐴)) → ∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |
46 | 7, 39, 45 | sylc 65 |
. . 3
⊢ ((𝑋 = 𝑌 ∧ 𝐵Ref𝐴) → ∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) |
47 | 46 | ex 416 |
. 2
⊢ (𝑋 = 𝑌 → (𝐵Ref𝐴 → ∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |
48 | | vex 3412 |
. . . . . . . 8
⊢ 𝑐 ∈ V |
49 | 48 | ssex 5214 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝑐 → 𝐵 ∈ V) |
50 | 49 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐵 ∈ V) |
51 | | simprl 771 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐵 ⊆ 𝑐) |
52 | | simpl 486 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑋 = 𝑌) |
53 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ 𝑐 =
∪ 𝑐 |
54 | 53, 17 | refbas 22407 |
. . . . . . . . 9
⊢ (𝑐Ref𝐴 → 𝑋 = ∪ 𝑐) |
55 | 54 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴Fne𝑐 ∧ 𝑐Ref𝐴) → 𝑋 = ∪ 𝑐) |
56 | 55 | ad2antll 729 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑋 = ∪ 𝑐) |
57 | 52, 56 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑌 = ∪ 𝑐) |
58 | 18, 53 | ssref 22409 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐵 ⊆ 𝑐 ∧ 𝑌 = ∪ 𝑐) → 𝐵Ref𝑐) |
59 | 50, 51, 57, 58 | syl3anc 1373 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐵Ref𝑐) |
60 | | simprrr 782 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑐Ref𝐴) |
61 | | reftr 22411 |
. . . . 5
⊢ ((𝐵Ref𝑐 ∧ 𝑐Ref𝐴) → 𝐵Ref𝐴) |
62 | 59, 60, 61 | syl2anc 587 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ (𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐵Ref𝐴) |
63 | 62 | ex 416 |
. . 3
⊢ (𝑋 = 𝑌 → ((𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) → 𝐵Ref𝐴)) |
64 | 63 | exlimdv 1941 |
. 2
⊢ (𝑋 = 𝑌 → (∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) → 𝐵Ref𝐴)) |
65 | 47, 64 | impbid 215 |
1
⊢ (𝑋 = 𝑌 → (𝐵Ref𝐴 ↔ ∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |