| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ⊆ 𝐴) | 
| 2 |  | velpw 4604 | . . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | 
| 3 | 1, 2 | sylibr 234 | . . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴) | 
| 4 |  | simp2 1137 | . . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥)) | 
| 5 |  | xpss12 5699 | . . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴)) | 
| 6 | 1, 1, 5 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴)) | 
| 7 | 4, 6 | sstrd 3993 | . . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴)) | 
| 8 |  | velpw 4604 | . . . . . . . 8
⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴)) | 
| 9 | 7, 8 | sylibr 234 | . . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) | 
| 10 | 3, 9 | jca 511 | . . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴))) | 
| 11 | 10 | ssopab2i 5554 | . . . . 5
⊢
{〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {〈𝑥, 𝑟〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴))} | 
| 12 |  | canthwe.1 | . . . . 5
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} | 
| 13 |  | df-xp 5690 | . . . . 5
⊢
(𝒫 𝐴 ×
𝒫 (𝐴 × 𝐴)) = {〈𝑥, 𝑟〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴))} | 
| 14 | 11, 12, 13 | 3sstr4i 4034 | . . . 4
⊢ 𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) | 
| 15 |  | pwexg 5377 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | 
| 16 |  | sqxpexg 7776 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | 
| 17 | 16 | pwexd 5378 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V) | 
| 18 | 15, 17 | xpexd 7772 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) | 
| 19 |  | ssexg 5322 | . . . 4
⊢ ((𝑂 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) ∈ V) → 𝑂 ∈ V) | 
| 20 | 14, 18, 19 | sylancr 587 | . . 3
⊢ (𝐴 ∈ 𝑉 → 𝑂 ∈ V) | 
| 21 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐴) | 
| 22 | 21 | snssd 4808 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → {𝑢} ⊆ 𝐴) | 
| 23 |  | 0ss 4399 | . . . . . . . 8
⊢ ∅
⊆ ({𝑢} × {𝑢}) | 
| 24 | 23 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → ∅ ⊆ ({𝑢} × {𝑢})) | 
| 25 |  | rel0 5808 | . . . . . . . 8
⊢ Rel
∅ | 
| 26 |  | br0 5191 | . . . . . . . . 9
⊢  ¬
𝑢∅𝑢 | 
| 27 |  | wesn 5773 | . . . . . . . . 9
⊢ (Rel
∅ → (∅ We {𝑢} ↔ ¬ 𝑢∅𝑢)) | 
| 28 | 26, 27 | mpbiri 258 | . . . . . . . 8
⊢ (Rel
∅ → ∅ We {𝑢}) | 
| 29 | 25, 28 | mp1i 13 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → ∅ We {𝑢}) | 
| 30 |  | vsnex 5433 | . . . . . . . 8
⊢ {𝑢} ∈ V | 
| 31 |  | 0ex 5306 | . . . . . . . 8
⊢ ∅
∈ V | 
| 32 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑥 = {𝑢}) | 
| 33 | 32 | sseq1d 4014 | . . . . . . . . 9
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 ⊆ 𝐴 ↔ {𝑢} ⊆ 𝐴)) | 
| 34 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → 𝑟 = ∅) | 
| 35 | 32 | sqxpeqd 5716 | . . . . . . . . . 10
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑥 × 𝑥) = ({𝑢} × {𝑢})) | 
| 36 | 34, 35 | sseq12d 4016 | . . . . . . . . 9
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ∅ ⊆ ({𝑢} × {𝑢}))) | 
| 37 | 34, 32 | weeq12d 5673 | . . . . . . . . 9
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → (𝑟 We 𝑥 ↔ ∅ We {𝑢})) | 
| 38 | 33, 36, 37 | 3anbi123d 1437 | . . . . . . . 8
⊢ ((𝑥 = {𝑢} ∧ 𝑟 = ∅) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢}))) | 
| 39 | 30, 31, 38 | opelopaba 5540 | . . . . . . 7
⊢
(〈{𝑢},
∅〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ ({𝑢} ⊆ 𝐴 ∧ ∅ ⊆ ({𝑢} × {𝑢}) ∧ ∅ We {𝑢})) | 
| 40 | 22, 24, 29, 39 | syl3anbrc 1343 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → 〈{𝑢}, ∅〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}) | 
| 41 | 40, 12 | eleqtrrdi 2851 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑢 ∈ 𝐴) → 〈{𝑢}, ∅〉 ∈ 𝑂) | 
| 42 | 41 | ex 412 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑢 ∈ 𝐴 → 〈{𝑢}, ∅〉 ∈ 𝑂)) | 
| 43 |  | eqid 2736 | . . . . . . 7
⊢ ∅ =
∅ | 
| 44 |  | vsnex 5433 | . . . . . . . 8
⊢ {𝑣} ∈ V | 
| 45 | 44, 31 | opth2 5484 | . . . . . . 7
⊢
(〈{𝑢},
∅〉 = 〈{𝑣},
∅〉 ↔ ({𝑢} =
{𝑣} ∧ ∅ =
∅)) | 
| 46 | 43, 45 | mpbiran2 710 | . . . . . 6
⊢
(〈{𝑢},
∅〉 = 〈{𝑣},
∅〉 ↔ {𝑢} =
{𝑣}) | 
| 47 |  | sneqbg 4842 | . . . . . . 7
⊢ (𝑢 ∈ V → ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣)) | 
| 48 | 47 | elv 3484 | . . . . . 6
⊢ ({𝑢} = {𝑣} ↔ 𝑢 = 𝑣) | 
| 49 | 46, 48 | bitri 275 | . . . . 5
⊢
(〈{𝑢},
∅〉 = 〈{𝑣},
∅〉 ↔ 𝑢 =
𝑣) | 
| 50 | 49 | 2a1i 12 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (〈{𝑢}, ∅〉 = 〈{𝑣}, ∅〉 ↔ 𝑢 = 𝑣))) | 
| 51 | 42, 50 | dom2d 9034 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝑂 ∈ V → 𝐴 ≼ 𝑂)) | 
| 52 | 20, 51 | mpd 15 | . 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝑂) | 
| 53 |  | eqid 2736 | . . . . . . 7
⊢
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} | 
| 54 | 53 | fpwwe2cbv 10671 | . . . . . 6
⊢
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑤](𝑤𝑓(𝑟 ∩ (𝑤 × 𝑤))) = 𝑦))} | 
| 55 |  | eqid 2736 | . . . . . 6
⊢ ∪ dom {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} = ∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} | 
| 56 |  | eqid 2736 | . . . . . 6
⊢ (◡({〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {(∪
dom {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) = (◡({〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}) “ {(∪
dom {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}𝑓({〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}‘∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝑓(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}))}) | 
| 57 | 12, 54, 55, 56 | canthwelem 10691 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ¬ 𝑓:𝑂–1-1→𝐴) | 
| 58 |  | f1of1 6846 | . . . . 5
⊢ (𝑓:𝑂–1-1-onto→𝐴 → 𝑓:𝑂–1-1→𝐴) | 
| 59 | 57, 58 | nsyl 140 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ¬ 𝑓:𝑂–1-1-onto→𝐴) | 
| 60 | 59 | nexdv 1935 | . . 3
⊢ (𝐴 ∈ 𝑉 → ¬ ∃𝑓 𝑓:𝑂–1-1-onto→𝐴) | 
| 61 |  | ensym 9044 | . . . 4
⊢ (𝐴 ≈ 𝑂 → 𝑂 ≈ 𝐴) | 
| 62 |  | bren 8996 | . . . 4
⊢ (𝑂 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝑂–1-1-onto→𝐴) | 
| 63 | 61, 62 | sylib 218 | . . 3
⊢ (𝐴 ≈ 𝑂 → ∃𝑓 𝑓:𝑂–1-1-onto→𝐴) | 
| 64 | 60, 63 | nsyl 140 | . 2
⊢ (𝐴 ∈ 𝑉 → ¬ 𝐴 ≈ 𝑂) | 
| 65 |  | brsdom 9016 | . 2
⊢ (𝐴 ≺ 𝑂 ↔ (𝐴 ≼ 𝑂 ∧ ¬ 𝐴 ≈ 𝑂)) | 
| 66 | 52, 64, 65 | sylanbrc 583 | 1
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂) |