Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pw2f1ocnv Structured version   Visualization version   GIF version

Theorem pw2f1ocnv 39894
 Description: Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8620, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.)
Hypothesis
Ref Expression
pw2f1o2.f 𝐹 = (𝑥 ∈ (2om 𝐴) ↦ (𝑥 “ {1o}))
Assertion
Ref Expression
pw2f1ocnv (𝐴𝑉 → (𝐹:(2om 𝐴)–1-1-onto→𝒫 𝐴𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝑉,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦,𝑧)   𝑉(𝑧)

Proof of Theorem pw2f1ocnv
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 pw2f1o2.f . 2 𝐹 = (𝑥 ∈ (2om 𝐴) ↦ (𝑥 “ {1o}))
2 vex 3483 . . . 4 𝑥 ∈ V
32cnvex 7625 . . 3 𝑥 ∈ V
4 imaexg 7615 . . 3 (𝑥 ∈ V → (𝑥 “ {1o}) ∈ V)
53, 4mp1i 13 . 2 ((𝐴𝑉𝑥 ∈ (2om 𝐴)) → (𝑥 “ {1o}) ∈ V)
6 mptexg 6975 . . 3 (𝐴𝑉 → (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) ∈ V)
76adantr 484 . 2 ((𝐴𝑉𝑦 ∈ 𝒫 𝐴) → (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) ∈ V)
8 2on 8107 . . . . . 6 2o ∈ On
9 elmapg 8415 . . . . . 6 ((2o ∈ On ∧ 𝐴𝑉) → (𝑥 ∈ (2om 𝐴) ↔ 𝑥:𝐴⟶2o))
108, 9mpan 689 . . . . 5 (𝐴𝑉 → (𝑥 ∈ (2om 𝐴) ↔ 𝑥:𝐴⟶2o))
1110anbi1d 632 . . . 4 (𝐴𝑉 → ((𝑥 ∈ (2om 𝐴) ∧ 𝑦 = (𝑥 “ {1o})) ↔ (𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o}))))
12 1oex 8106 . . . . . . . . . . . 12 1o ∈ V
1312sucid 6257 . . . . . . . . . . 11 1o ∈ suc 1o
14 df-2o 8099 . . . . . . . . . . 11 2o = suc 1o
1513, 14eleqtrri 2915 . . . . . . . . . 10 1o ∈ 2o
16 0ex 5197 . . . . . . . . . . . 12 ∅ ∈ V
1716prid1 4683 . . . . . . . . . . 11 ∅ ∈ {∅, {∅}}
18 df2o2 8114 . . . . . . . . . . 11 2o = {∅, {∅}}
1917, 18eleqtrri 2915 . . . . . . . . . 10 ∅ ∈ 2o
2015, 19ifcli 4496 . . . . . . . . 9 if(𝑧𝑦, 1o, ∅) ∈ 2o
2120rgenw 3145 . . . . . . . 8 𝑧𝐴 if(𝑧𝑦, 1o, ∅) ∈ 2o
22 eqid 2824 . . . . . . . . 9 (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))
2322fmpt 6865 . . . . . . . 8 (∀𝑧𝐴 if(𝑧𝑦, 1o, ∅) ∈ 2o ↔ (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)):𝐴⟶2o)
2421, 23mpbi 233 . . . . . . 7 (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)):𝐴⟶2o
25 simpr 488 . . . . . . . 8 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → 𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))
2625feq1d 6488 . . . . . . 7 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o ↔ (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)):𝐴⟶2o))
2724, 26mpbiri 261 . . . . . 6 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → 𝑥:𝐴⟶2o)
2825fveq1d 6663 . . . . . . . . . . . . 13 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑥𝑤) = ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤))
29 elequ1 2122 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (𝑧𝑦𝑤𝑦))
3029ifbid 4472 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → if(𝑧𝑦, 1o, ∅) = if(𝑤𝑦, 1o, ∅))
3112, 16ifcli 4496 . . . . . . . . . . . . . 14 if(𝑤𝑦, 1o, ∅) ∈ V
3230, 22, 31fvmpt 6759 . . . . . . . . . . . . 13 (𝑤𝐴 → ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤) = if(𝑤𝑦, 1o, ∅))
3328, 32sylan9eq 2879 . . . . . . . . . . . 12 (((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ∧ 𝑤𝐴) → (𝑥𝑤) = if(𝑤𝑦, 1o, ∅))
3433eqeq1d 2826 . . . . . . . . . . 11 (((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ∧ 𝑤𝐴) → ((𝑥𝑤) = 1o ↔ if(𝑤𝑦, 1o, ∅) = 1o))
35 iftrue 4456 . . . . . . . . . . . 12 (𝑤𝑦 → if(𝑤𝑦, 1o, ∅) = 1o)
36 noel 4280 . . . . . . . . . . . . . 14 ¬ ∅ ∈ ∅
37 iffalse 4459 . . . . . . . . . . . . . . . 16 𝑤𝑦 → if(𝑤𝑦, 1o, ∅) = ∅)
3837eqeq1d 2826 . . . . . . . . . . . . . . 15 𝑤𝑦 → (if(𝑤𝑦, 1o, ∅) = 1o ↔ ∅ = 1o))
39 0lt1o 8125 . . . . . . . . . . . . . . . 16 ∅ ∈ 1o
40 eleq2 2904 . . . . . . . . . . . . . . . 16 (∅ = 1o → (∅ ∈ ∅ ↔ ∅ ∈ 1o))
4139, 40mpbiri 261 . . . . . . . . . . . . . . 15 (∅ = 1o → ∅ ∈ ∅)
4238, 41syl6bi 256 . . . . . . . . . . . . . 14 𝑤𝑦 → (if(𝑤𝑦, 1o, ∅) = 1o → ∅ ∈ ∅))
4336, 42mtoi 202 . . . . . . . . . . . . 13 𝑤𝑦 → ¬ if(𝑤𝑦, 1o, ∅) = 1o)
4443con4i 114 . . . . . . . . . . . 12 (if(𝑤𝑦, 1o, ∅) = 1o𝑤𝑦)
4535, 44impbii 212 . . . . . . . . . . 11 (𝑤𝑦 ↔ if(𝑤𝑦, 1o, ∅) = 1o)
4634, 45syl6rbbr 293 . . . . . . . . . 10 (((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ∧ 𝑤𝐴) → (𝑤𝑦 ↔ (𝑥𝑤) = 1o))
47 fvex 6674 . . . . . . . . . . 11 (𝑥𝑤) ∈ V
4847elsn 4565 . . . . . . . . . 10 ((𝑥𝑤) ∈ {1o} ↔ (𝑥𝑤) = 1o)
4946, 48syl6bbr 292 . . . . . . . . 9 (((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ∧ 𝑤𝐴) → (𝑤𝑦 ↔ (𝑥𝑤) ∈ {1o}))
5049pm5.32da 582 . . . . . . . 8 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → ((𝑤𝐴𝑤𝑦) ↔ (𝑤𝐴 ∧ (𝑥𝑤) ∈ {1o})))
51 ssel 3946 . . . . . . . . . 10 (𝑦𝐴 → (𝑤𝑦𝑤𝐴))
5251adantr 484 . . . . . . . . 9 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑤𝑦𝑤𝐴))
5352pm4.71rd 566 . . . . . . . 8 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑤𝑦 ↔ (𝑤𝐴𝑤𝑦)))
54 ffn 6503 . . . . . . . . 9 (𝑥:𝐴⟶2o𝑥 Fn 𝐴)
55 elpreima 6819 . . . . . . . . 9 (𝑥 Fn 𝐴 → (𝑤 ∈ (𝑥 “ {1o}) ↔ (𝑤𝐴 ∧ (𝑥𝑤) ∈ {1o})))
5627, 54, 553syl 18 . . . . . . . 8 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑤 ∈ (𝑥 “ {1o}) ↔ (𝑤𝐴 ∧ (𝑥𝑤) ∈ {1o})))
5750, 53, 563bitr4d 314 . . . . . . 7 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑤𝑦𝑤 ∈ (𝑥 “ {1o})))
5857eqrdv 2822 . . . . . 6 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → 𝑦 = (𝑥 “ {1o}))
5927, 58jca 515 . . . . 5 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})))
60 simpr 488 . . . . . . 7 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → 𝑦 = (𝑥 “ {1o}))
61 cnvimass 5936 . . . . . . . 8 (𝑥 “ {1o}) ⊆ dom 𝑥
62 fdm 6511 . . . . . . . . 9 (𝑥:𝐴⟶2o → dom 𝑥 = 𝐴)
6362adantr 484 . . . . . . . 8 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → dom 𝑥 = 𝐴)
6461, 63sseqtrid 4005 . . . . . . 7 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → (𝑥 “ {1o}) ⊆ 𝐴)
6560, 64eqsstrd 3991 . . . . . 6 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → 𝑦𝐴)
66 simplr 768 . . . . . . . . . . . . . 14 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → 𝑦 = (𝑥 “ {1o}))
6766eleq2d 2901 . . . . . . . . . . . . 13 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑤𝑦𝑤 ∈ (𝑥 “ {1o})))
6854adantr 484 . . . . . . . . . . . . . . 15 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → 𝑥 Fn 𝐴)
69 fnbrfvb 6709 . . . . . . . . . . . . . . 15 ((𝑥 Fn 𝐴𝑤𝐴) → ((𝑥𝑤) = 1o𝑤𝑥1o))
7068, 69sylan 583 . . . . . . . . . . . . . 14 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → ((𝑥𝑤) = 1o𝑤𝑥1o))
71 1on 8105 . . . . . . . . . . . . . . 15 1o ∈ On
72 vex 3483 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
7372eliniseg 5945 . . . . . . . . . . . . . . 15 (1o ∈ On → (𝑤 ∈ (𝑥 “ {1o}) ↔ 𝑤𝑥1o))
7471, 73ax-mp 5 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 “ {1o}) ↔ 𝑤𝑥1o)
7570, 74syl6bbr 292 . . . . . . . . . . . . 13 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → ((𝑥𝑤) = 1o𝑤 ∈ (𝑥 “ {1o})))
7667, 75bitr4d 285 . . . . . . . . . . . 12 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑤𝑦 ↔ (𝑥𝑤) = 1o))
7776biimpa 480 . . . . . . . . . . 11 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ 𝑤𝑦) → (𝑥𝑤) = 1o)
7835adantl 485 . . . . . . . . . . 11 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ 𝑤𝑦) → if(𝑤𝑦, 1o, ∅) = 1o)
7977, 78eqtr4d 2862 . . . . . . . . . 10 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ 𝑤𝑦) → (𝑥𝑤) = if(𝑤𝑦, 1o, ∅))
80 ffvelrn 6840 . . . . . . . . . . . . . . . . . 18 ((𝑥:𝐴⟶2o𝑤𝐴) → (𝑥𝑤) ∈ 2o)
8180adantlr 714 . . . . . . . . . . . . . . . . 17 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑥𝑤) ∈ 2o)
82 df2o3 8113 . . . . . . . . . . . . . . . . 17 2o = {∅, 1o}
8381, 82eleqtrdi 2926 . . . . . . . . . . . . . . . 16 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑥𝑤) ∈ {∅, 1o})
8447elpr 4573 . . . . . . . . . . . . . . . 16 ((𝑥𝑤) ∈ {∅, 1o} ↔ ((𝑥𝑤) = ∅ ∨ (𝑥𝑤) = 1o))
8583, 84sylib 221 . . . . . . . . . . . . . . 15 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → ((𝑥𝑤) = ∅ ∨ (𝑥𝑤) = 1o))
8685ord 861 . . . . . . . . . . . . . 14 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (¬ (𝑥𝑤) = ∅ → (𝑥𝑤) = 1o))
8786, 76sylibrd 262 . . . . . . . . . . . . 13 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (¬ (𝑥𝑤) = ∅ → 𝑤𝑦))
8887con1d 147 . . . . . . . . . . . 12 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (¬ 𝑤𝑦 → (𝑥𝑤) = ∅))
8988imp 410 . . . . . . . . . . 11 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ ¬ 𝑤𝑦) → (𝑥𝑤) = ∅)
9037adantl 485 . . . . . . . . . . 11 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ ¬ 𝑤𝑦) → if(𝑤𝑦, 1o, ∅) = ∅)
9189, 90eqtr4d 2862 . . . . . . . . . 10 ((((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) ∧ ¬ 𝑤𝑦) → (𝑥𝑤) = if(𝑤𝑦, 1o, ∅))
9279, 91pm2.61dan 812 . . . . . . . . 9 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑥𝑤) = if(𝑤𝑦, 1o, ∅))
9332adantl 485 . . . . . . . . 9 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤) = if(𝑤𝑦, 1o, ∅))
9492, 93eqtr4d 2862 . . . . . . . 8 (((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) ∧ 𝑤𝐴) → (𝑥𝑤) = ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤))
9594ralrimiva 3177 . . . . . . 7 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → ∀𝑤𝐴 (𝑥𝑤) = ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤))
96 ffn 6503 . . . . . . . . 9 ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)):𝐴⟶2o → (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) Fn 𝐴)
9724, 96ax-mp 5 . . . . . . . 8 (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) Fn 𝐴
98 eqfnfv 6793 . . . . . . . 8 ((𝑥 Fn 𝐴 ∧ (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) Fn 𝐴) → (𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) ↔ ∀𝑤𝐴 (𝑥𝑤) = ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤)))
9968, 97, 98sylancl 589 . . . . . . 7 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → (𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)) ↔ ∀𝑤𝐴 (𝑥𝑤) = ((𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))‘𝑤)))
10095, 99mpbird 260 . . . . . 6 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → 𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))
10165, 100jca 515 . . . . 5 ((𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})) → (𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))))
10259, 101impbii 212 . . . 4 ((𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ↔ (𝑥:𝐴⟶2o𝑦 = (𝑥 “ {1o})))
10311, 102syl6bbr 292 . . 3 (𝐴𝑉 → ((𝑥 ∈ (2om 𝐴) ∧ 𝑦 = (𝑥 “ {1o})) ↔ (𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))))
104 velpw 4527 . . . 4 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
105104anbi1i 626 . . 3 ((𝑦 ∈ 𝒫 𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))) ↔ (𝑦𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅))))
106103, 105syl6bbr 292 . 2 (𝐴𝑉 → ((𝑥 ∈ (2om 𝐴) ∧ 𝑦 = (𝑥 “ {1o})) ↔ (𝑦 ∈ 𝒫 𝐴𝑥 = (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))))
1071, 5, 7, 106f1ocnvd 7390 1 (𝐴𝑉 → (𝐹:(2om 𝐴)–1-1-onto→𝒫 𝐴𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧𝐴 ↦ if(𝑧𝑦, 1o, ∅)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115  ∀wral 3133  Vcvv 3480   ⊆ wss 3919  ∅c0 4276  ifcif 4450  𝒫 cpw 4522  {csn 4550  {cpr 4552   class class class wbr 5052   ↦ cmpt 5132  ◡ccnv 5541  dom cdm 5542   “ cima 5545  Oncon0 6178  suc csuc 6180   Fn wfn 6338  ⟶wf 6339  –1-1-onto→wf1o 6342  ‘cfv 6343  (class class class)co 7149  1oc1o 8091  2oc2o 8092   ↑m cmap 8402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-ord 6181  df-on 6182  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1o 8098  df-2o 8099  df-map 8404 This theorem is referenced by:  pw2f1o2  39895
 Copyright terms: Public domain W3C validator