| Step | Hyp | Ref
| Expression |
| 1 | | wunfi.2 |
. 2
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
| 2 | | wunfi.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 3 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝑈 ↔ ∅ ⊆ 𝑈)) |
| 4 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝑈 ↔ ∅ ∈ 𝑈)) |
| 5 | 3, 4 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈) ↔ (∅ ⊆ 𝑈 → ∅ ∈ 𝑈))) |
| 6 | 5 | imbi2d 340 |
. . . 4
⊢ (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈)) ↔ (𝜑 → (∅ ⊆ 𝑈 → ∅ ∈ 𝑈)))) |
| 7 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝑈 ↔ 𝑦 ⊆ 𝑈)) |
| 8 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑈 ↔ 𝑦 ∈ 𝑈)) |
| 9 | 7, 8 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈) ↔ (𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈))) |
| 10 | 9 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈)) ↔ (𝜑 → (𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈)))) |
| 11 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝑈 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝑈)) |
| 12 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ 𝑈 ↔ (𝑦 ∪ {𝑧}) ∈ 𝑈)) |
| 13 | 11, 12 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈))) |
| 14 | 13 | imbi2d 340 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈)) ↔ (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈)))) |
| 15 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑈 ↔ 𝐴 ⊆ 𝑈)) |
| 16 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈)) |
| 17 | 15, 16 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈) ↔ (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈))) |
| 18 | 17 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝜑 → (𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈)) ↔ (𝜑 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈)))) |
| 19 | | wun0.1 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 20 | 19 | wun0 10758 |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝑈) |
| 21 | 20 | a1d 25 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝑈 → ∅ ∈ 𝑈)) |
| 22 | | ssun1 4178 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
| 23 | | sstr 3992 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑈) → 𝑦 ⊆ 𝑈) |
| 24 | 22, 23 | mpan 690 |
. . . . . . . 8
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → 𝑦 ⊆ 𝑈) |
| 25 | 24 | imim1i 63 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈) → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → 𝑦 ∈ 𝑈)) |
| 26 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑈 ∈ WUni) |
| 27 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈) |
| 28 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∪ {𝑧}) ⊆ 𝑈) |
| 29 | 28 | unssbd 4194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → {𝑧} ⊆ 𝑈) |
| 30 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
| 31 | 30 | snss 4785 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑈 ↔ {𝑧} ⊆ 𝑈) |
| 32 | 29, 31 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑧 ∈ 𝑈) |
| 33 | 26, 32 | wunsn 10756 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → {𝑧} ∈ 𝑈) |
| 34 | 26, 27, 33 | wunun 10750 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑦 ∪ {𝑧}) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑦 ∪ {𝑧}) ∈ 𝑈) |
| 35 | 34 | exp32 420 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∈ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈))) |
| 36 | 35 | a2d 29 |
. . . . . . 7
⊢ (𝜑 → (((𝑦 ∪ {𝑧}) ⊆ 𝑈 → 𝑦 ∈ 𝑈) → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈))) |
| 37 | 25, 36 | syl5 34 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈) → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈))) |
| 38 | 37 | a2i 14 |
. . . . 5
⊢ ((𝜑 → (𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈))) |
| 39 | 38 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ Fin → ((𝜑 → (𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝑈 → (𝑦 ∪ {𝑧}) ∈ 𝑈)))) |
| 40 | 6, 10, 14, 18, 21, 39 | findcard2 9204 |
. . 3
⊢ (𝐴 ∈ Fin → (𝜑 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈))) |
| 41 | 2, 40 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈)) |
| 42 | 1, 41 | mpd 15 |
1
⊢ (𝜑 → 𝐴 ∈ 𝑈) |