| Step | Hyp | Ref
| Expression |
| 1 | | fnerel 36339 |
. . . . . . 7
⊢ Rel
Fne |
| 2 | 1 | brrelex2i 5742 |
. . . . . 6
⊢ (𝐴Fne𝐵 → 𝐵 ∈ V) |
| 3 | 2 | adantl 481 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → 𝐵 ∈ V) |
| 4 | | rabexg 5337 |
. . . . 5
⊢ (𝐵 ∈ V → {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V) |
| 6 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵 |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵) |
| 8 | | fnessref.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = ∪
𝐴 |
| 9 | 8 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝐴) |
| 10 | | eluni 4910 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ∪ 𝐴
↔ ∃𝑧(𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)) |
| 11 | 9, 10 | bitri 275 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝑋 ↔ ∃𝑧(𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)) |
| 12 | | fnessex 36347 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴Fne𝐵 ∧ 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧) → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧)) |
| 13 | 12 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴Fne𝐵 ∧ 𝑧 ∈ 𝐴) → (𝑡 ∈ 𝑧 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧))) |
| 14 | 13 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ 𝑧 ∈ 𝐴) → (𝑡 ∈ 𝑧 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧))) |
| 15 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑧)) |
| 16 | 15 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑧) → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
| 17 | 16 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐴 → (𝑥 ⊆ 𝑧 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ 𝑧 ∈ 𝐴) → (𝑥 ⊆ 𝑧 → ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
| 19 | 18 | anim2d 612 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ 𝑧 ∈ 𝐴) → ((𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧) → (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 20 | 19 | reximdv 3170 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ 𝑧 ∈ 𝐴) → (∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑧) → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 21 | 14, 20 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ 𝑧 ∈ 𝐴) → (𝑡 ∈ 𝑧 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 22 | 21 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝑧 ∈ 𝐴 → (𝑡 ∈ 𝑧 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)))) |
| 23 | 22 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝑡 ∈ 𝑧 → (𝑧 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)))) |
| 24 | 23 | impd 410 |
. . . . . . . . . . 11
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ((𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 25 | 24 | exlimdv 1933 |
. . . . . . . . . 10
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (∃𝑧(𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 26 | 11, 25 | biimtrid 242 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝑡 ∈ 𝑋 → ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦))) |
| 27 | | elunirab 4922 |
. . . . . . . . 9
⊢ (𝑡 ∈ ∪ {𝑥
∈ 𝐵 ∣
∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ↔ ∃𝑥 ∈ 𝐵 (𝑡 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦)) |
| 28 | 26, 27 | imbitrrdi 252 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝑡 ∈ 𝑋 → 𝑡 ∈ ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})) |
| 29 | 28 | ssrdv 3989 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → 𝑋 ⊆ ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}) |
| 30 | 6 | unissi 4916 |
. . . . . . . 8
⊢ ∪ {𝑥
∈ 𝐵 ∣
∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ ∪ 𝐵 |
| 31 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → 𝑋 = 𝑌) |
| 32 | | fnessref.2 |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐵 |
| 33 | 31, 32 | eqtr2di 2794 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ∪ 𝐵 = 𝑋) |
| 34 | 30, 33 | sseqtrid 4026 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝑋) |
| 35 | 29, 34 | eqssd 4001 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → 𝑋 = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}) |
| 36 | | fnessex 36347 |
. . . . . . . . . 10
⊢ ((𝐴Fne𝐵 ∧ 𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧) → ∃𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 37 | 36 | 3expb 1121 |
. . . . . . . . 9
⊢ ((𝐴Fne𝐵 ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ∃𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 38 | 37 | adantll 714 |
. . . . . . . 8
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ∃𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 39 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → 𝑤 ∈ 𝐵) |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → 𝑤 ∈ 𝐵)) |
| 41 | | sseq2 4010 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝑤 ⊆ 𝑦 ↔ 𝑤 ⊆ 𝑧)) |
| 42 | 41 | rspcev 3622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ⊆ 𝑧) → ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦) |
| 43 | 42 | expcom 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ⊆ 𝑧 → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 44 | 43 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 45 | 44 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 46 | 45 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 47 | 40, 46 | jcad 512 |
. . . . . . . . . . 11
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → (𝑤 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦))) |
| 48 | | sseq1 4009 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥 ⊆ 𝑦 ↔ 𝑤 ⊆ 𝑦)) |
| 49 | 48 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 50 | 49 | elrab 3692 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ↔ (𝑤 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐴 𝑤 ⊆ 𝑦)) |
| 51 | 47, 50 | imbitrrdi 252 |
. . . . . . . . . 10
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → 𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})) |
| 52 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 53 | 52 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
| 54 | 51, 53 | jcad 512 |
. . . . . . . . 9
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ((𝑤 ∈ 𝐵 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) → (𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
| 55 | 54 | reximdv2 3164 |
. . . . . . . 8
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → (∃𝑤 ∈ 𝐵 (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) → ∃𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
| 56 | 38, 55 | mpd 15 |
. . . . . . 7
⊢ (((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑡 ∈ 𝑧)) → ∃𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 57 | 56 | ralrimivva 3202 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ 𝑧 ∃𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
| 58 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ {𝑥
∈ 𝐵 ∣
∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} |
| 59 | 8, 58 | isfne2 36343 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V → (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ↔ (𝑋 = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ 𝑧 ∃𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
| 60 | 3, 4, 59 | 3syl 18 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ↔ (𝑋 = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ ∀𝑧 ∈ 𝐴 ∀𝑡 ∈ 𝑧 ∃𝑤 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} (𝑡 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
| 61 | 35, 57, 60 | mpbir2and 713 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → 𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}) |
| 62 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑦)) |
| 63 | 62 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦)) |
| 64 | 63 | elrab 3692 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ↔ (𝑧 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦)) |
| 65 | | sseq2 4010 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ 𝑤)) |
| 66 | 65 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐴 𝑧 ⊆ 𝑦 ↔ ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
| 67 | 66 | biimpi 216 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐴 𝑧 ⊆ 𝑦 → ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
| 68 | 67 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦) → ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
| 69 | 68 | a1i 11 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ((𝑧 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐴 𝑧 ⊆ 𝑦) → ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤)) |
| 70 | 64, 69 | biimtrid 242 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤)) |
| 71 | 70 | ralrimiv 3145 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) |
| 72 | 58, 8 | isref 23517 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V → ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴 ↔ (𝑋 = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤))) |
| 73 | 3, 4, 72 | 3syl 18 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴 ↔ (𝑋 = ∪ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤))) |
| 74 | 35, 71, 73 | mpbir2and 713 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴) |
| 75 | 7, 61, 74 | jca32 515 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵 ∧ (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴))) |
| 76 | | sseq1 4009 |
. . . . . 6
⊢ (𝑐 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → (𝑐 ⊆ 𝐵 ↔ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵)) |
| 77 | | breq2 5147 |
. . . . . . 7
⊢ (𝑐 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → (𝐴Fne𝑐 ↔ 𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦})) |
| 78 | | breq1 5146 |
. . . . . . 7
⊢ (𝑐 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → (𝑐Ref𝐴 ↔ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴)) |
| 79 | 77, 78 | anbi12d 632 |
. . . . . 6
⊢ (𝑐 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → ((𝐴Fne𝑐 ∧ 𝑐Ref𝐴) ↔ (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴))) |
| 80 | 76, 79 | anbi12d 632 |
. . . . 5
⊢ (𝑐 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} → ((𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) ↔ ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵 ∧ (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴)))) |
| 81 | 80 | spcegv 3597 |
. . . 4
⊢ ({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V → (({𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ⊆ 𝐵 ∧ (𝐴Fne{𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∧ {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦}Ref𝐴)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |
| 82 | 5, 75, 81 | sylc 65 |
. . 3
⊢ ((𝑋 = 𝑌 ∧ 𝐴Fne𝐵) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) |
| 83 | 82 | ex 412 |
. 2
⊢ (𝑋 = 𝑌 → (𝐴Fne𝐵 → ∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |
| 84 | | simprrl 781 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐴Fne𝑐) |
| 85 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ∪ 𝑐 =
∪ 𝑐 |
| 86 | 8, 85 | fnebas 36345 |
. . . . . . . . . . 11
⊢ (𝐴Fne𝑐 → 𝑋 = ∪ 𝑐) |
| 87 | 84, 86 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑋 = ∪ 𝑐) |
| 88 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑋 = 𝑌) |
| 89 | 87, 88 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → ∪
𝑐 = 𝑌) |
| 90 | 89, 32 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → ∪
𝑐 = ∪ 𝐵) |
| 91 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑐
∈ V |
| 92 | 90, 91 | eqeltrrdi 2850 |
. . . . . . 7
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → ∪
𝐵 ∈
V) |
| 93 | | uniexb 7784 |
. . . . . . 7
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) |
| 94 | 92, 93 | sylibr 234 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐵 ∈ V) |
| 95 | | simprl 771 |
. . . . . 6
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑐 ⊆ 𝐵) |
| 96 | 85, 32 | fness 36350 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑐 ⊆ 𝐵 ∧ ∪ 𝑐 = 𝑌) → 𝑐Fne𝐵) |
| 97 | 94, 95, 89, 96 | syl3anc 1373 |
. . . . 5
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝑐Fne𝐵) |
| 98 | | fnetr 36352 |
. . . . 5
⊢ ((𝐴Fne𝑐 ∧ 𝑐Fne𝐵) → 𝐴Fne𝐵) |
| 99 | 84, 97, 98 | syl2anc 584 |
. . . 4
⊢ ((𝑋 = 𝑌 ∧ (𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))) → 𝐴Fne𝐵) |
| 100 | 99 | ex 412 |
. . 3
⊢ (𝑋 = 𝑌 → ((𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) → 𝐴Fne𝐵)) |
| 101 | 100 | exlimdv 1933 |
. 2
⊢ (𝑋 = 𝑌 → (∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)) → 𝐴Fne𝐵)) |
| 102 | 83, 101 | impbid 212 |
1
⊢ (𝑋 = 𝑌 → (𝐴Fne𝐵 ↔ ∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴)))) |