Metamath Proof Explorer


Theorem wepwsolem

Description: Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses wepwso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑧𝑦 ∧ ¬ 𝑧𝑥 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ) }
wepwso.u 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
wepwso.f 𝐹 = ( 𝑎 ∈ ( 2om 𝐴 ) ↦ ( 𝑎 “ { 1o } ) )
Assertion wepwsolem ( 𝐴 ∈ V → 𝐹 Isom 𝑈 , 𝑇 ( ( 2om 𝐴 ) , 𝒫 𝐴 ) )

Proof

Step Hyp Ref Expression
1 wepwso.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑧𝑦 ∧ ¬ 𝑧𝑥 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ) }
2 wepwso.u 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
3 wepwso.f 𝐹 = ( 𝑎 ∈ ( 2om 𝐴 ) ↦ ( 𝑎 “ { 1o } ) )
4 3 pw2f1o2 ( 𝐴 ∈ V → 𝐹 : ( 2om 𝐴 ) –1-1-onto→ 𝒫 𝐴 )
5 fvex ( 𝑐𝑧 ) ∈ V
6 5 epeli ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ↔ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) )
7 elmapi ( 𝑏 ∈ ( 2om 𝐴 ) → 𝑏 : 𝐴 ⟶ 2o )
8 7 ad2antrl ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) → 𝑏 : 𝐴 ⟶ 2o )
9 8 ffvelrnda ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( 𝑏𝑧 ) ∈ 2o )
10 elmapi ( 𝑐 ∈ ( 2om 𝐴 ) → 𝑐 : 𝐴 ⟶ 2o )
11 10 ad2antll ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) → 𝑐 : 𝐴 ⟶ 2o )
12 11 ffvelrnda ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( 𝑐𝑧 ) ∈ 2o )
13 n0i ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) → ¬ ( 𝑐𝑧 ) = ∅ )
14 13 adantl ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) → ¬ ( 𝑐𝑧 ) = ∅ )
15 elpri ( ( 𝑐𝑧 ) ∈ { ∅ , 1o } → ( ( 𝑐𝑧 ) = ∅ ∨ ( 𝑐𝑧 ) = 1o ) )
16 df2o3 2o = { ∅ , 1o }
17 15 16 eleq2s ( ( 𝑐𝑧 ) ∈ 2o → ( ( 𝑐𝑧 ) = ∅ ∨ ( 𝑐𝑧 ) = 1o ) )
18 17 ad2antlr ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) → ( ( 𝑐𝑧 ) = ∅ ∨ ( 𝑐𝑧 ) = 1o ) )
19 orel1 ( ¬ ( 𝑐𝑧 ) = ∅ → ( ( ( 𝑐𝑧 ) = ∅ ∨ ( 𝑐𝑧 ) = 1o ) → ( 𝑐𝑧 ) = 1o ) )
20 14 18 19 sylc ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) → ( 𝑐𝑧 ) = 1o )
21 1on 1o ∈ On
22 21 onirri ¬ 1o ∈ 1o
23 eleq12 ( ( ( 𝑏𝑧 ) = 1o ∧ ( 𝑐𝑧 ) = 1o ) → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ↔ 1o ∈ 1o ) )
24 23 biimpd ( ( ( 𝑏𝑧 ) = 1o ∧ ( 𝑐𝑧 ) = 1o ) → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) → 1o ∈ 1o ) )
25 24 expcom ( ( 𝑐𝑧 ) = 1o → ( ( 𝑏𝑧 ) = 1o → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) → 1o ∈ 1o ) ) )
26 25 com3r ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) → ( ( 𝑐𝑧 ) = 1o → ( ( 𝑏𝑧 ) = 1o → 1o ∈ 1o ) ) )
27 26 imp ( ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ∧ ( 𝑐𝑧 ) = 1o ) → ( ( 𝑏𝑧 ) = 1o → 1o ∈ 1o ) )
28 27 adantll ( ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) ∧ ( 𝑐𝑧 ) = 1o ) → ( ( 𝑏𝑧 ) = 1o → 1o ∈ 1o ) )
29 22 28 mtoi ( ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) ∧ ( 𝑐𝑧 ) = 1o ) → ¬ ( 𝑏𝑧 ) = 1o )
30 20 29 mpdan ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) → ¬ ( 𝑏𝑧 ) = 1o )
31 20 30 jca ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ) → ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) )
32 elpri ( ( 𝑏𝑧 ) ∈ { ∅ , 1o } → ( ( 𝑏𝑧 ) = ∅ ∨ ( 𝑏𝑧 ) = 1o ) )
33 32 16 eleq2s ( ( 𝑏𝑧 ) ∈ 2o → ( ( 𝑏𝑧 ) = ∅ ∨ ( 𝑏𝑧 ) = 1o ) )
34 33 adantr ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) → ( ( 𝑏𝑧 ) = ∅ ∨ ( 𝑏𝑧 ) = 1o ) )
35 orel2 ( ¬ ( 𝑏𝑧 ) = 1o → ( ( ( 𝑏𝑧 ) = ∅ ∨ ( 𝑏𝑧 ) = 1o ) → ( 𝑏𝑧 ) = ∅ ) )
36 34 35 mpan9 ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ¬ ( 𝑏𝑧 ) = 1o ) → ( 𝑏𝑧 ) = ∅ )
37 36 adantrl ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) → ( 𝑏𝑧 ) = ∅ )
38 0lt1o ∅ ∈ 1o
39 37 38 eqeltrdi ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) → ( 𝑏𝑧 ) ∈ 1o )
40 simprl ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) → ( 𝑐𝑧 ) = 1o )
41 39 40 eleqtrrd ( ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) ∧ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) → ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) )
42 31 41 impbida ( ( ( 𝑏𝑧 ) ∈ 2o ∧ ( 𝑐𝑧 ) ∈ 2o ) → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ↔ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) )
43 9 12 42 syl2anc ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ↔ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) )
44 simplrr ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → 𝑐 ∈ ( 2om 𝐴 ) )
45 3 pw2f1o2val2 ( ( 𝑐 ∈ ( 2om 𝐴 ) ∧ 𝑧𝐴 ) → ( 𝑧 ∈ ( 𝐹𝑐 ) ↔ ( 𝑐𝑧 ) = 1o ) )
46 44 45 sylancom ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( 𝑧 ∈ ( 𝐹𝑐 ) ↔ ( 𝑐𝑧 ) = 1o ) )
47 simplrl ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → 𝑏 ∈ ( 2om 𝐴 ) )
48 3 pw2f1o2val2 ( ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑧𝐴 ) → ( 𝑧 ∈ ( 𝐹𝑏 ) ↔ ( 𝑏𝑧 ) = 1o ) )
49 47 48 sylancom ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( 𝑧 ∈ ( 𝐹𝑏 ) ↔ ( 𝑏𝑧 ) = 1o ) )
50 49 notbid ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ¬ 𝑧 ∈ ( 𝐹𝑏 ) ↔ ¬ ( 𝑏𝑧 ) = 1o ) )
51 46 50 anbi12d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ↔ ( ( 𝑐𝑧 ) = 1o ∧ ¬ ( 𝑏𝑧 ) = 1o ) ) )
52 43 51 bitr4d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ( 𝑏𝑧 ) ∈ ( 𝑐𝑧 ) ↔ ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ) )
53 6 52 syl5bb ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ↔ ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ) )
54 8 ffvelrnda ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( 𝑏𝑤 ) ∈ 2o )
55 11 ffvelrnda ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( 𝑐𝑤 ) ∈ 2o )
56 eqeq1 ( ( 𝑏𝑤 ) = ( 𝑐𝑤 ) → ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) )
57 simplr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑏𝑤 ) = ∅ )
58 1n0 1o ≠ ∅
59 58 nesymi ¬ ∅ = 1o
60 eqeq1 ( ( 𝑏𝑤 ) = ∅ → ( ( 𝑏𝑤 ) = 1o ↔ ∅ = 1o ) )
61 59 60 mtbiri ( ( 𝑏𝑤 ) = ∅ → ¬ ( 𝑏𝑤 ) = 1o )
62 61 ad2antlr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ¬ ( 𝑏𝑤 ) = 1o )
63 simpr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) )
64 62 63 mtbid ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ¬ ( 𝑐𝑤 ) = 1o )
65 elpri ( ( 𝑐𝑤 ) ∈ { ∅ , 1o } → ( ( 𝑐𝑤 ) = ∅ ∨ ( 𝑐𝑤 ) = 1o ) )
66 65 16 eleq2s ( ( 𝑐𝑤 ) ∈ 2o → ( ( 𝑐𝑤 ) = ∅ ∨ ( 𝑐𝑤 ) = 1o ) )
67 66 ad3antlr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( ( 𝑐𝑤 ) = ∅ ∨ ( 𝑐𝑤 ) = 1o ) )
68 orel2 ( ¬ ( 𝑐𝑤 ) = 1o → ( ( ( 𝑐𝑤 ) = ∅ ∨ ( 𝑐𝑤 ) = 1o ) → ( 𝑐𝑤 ) = ∅ ) )
69 64 67 68 sylc ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑐𝑤 ) = ∅ )
70 57 69 eqtr4d ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) )
71 70 ex ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = ∅ ) → ( ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) )
72 simplr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = 1o ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑏𝑤 ) = 1o )
73 simpr ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = 1o ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) )
74 72 73 mpbid ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = 1o ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑐𝑤 ) = 1o )
75 72 74 eqtr4d ( ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = 1o ) ∧ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) )
76 75 ex ( ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) ∧ ( 𝑏𝑤 ) = 1o ) → ( ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) )
77 elpri ( ( 𝑏𝑤 ) ∈ { ∅ , 1o } → ( ( 𝑏𝑤 ) = ∅ ∨ ( 𝑏𝑤 ) = 1o ) )
78 77 16 eleq2s ( ( 𝑏𝑤 ) ∈ 2o → ( ( 𝑏𝑤 ) = ∅ ∨ ( 𝑏𝑤 ) = 1o ) )
79 78 adantr ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) → ( ( 𝑏𝑤 ) = ∅ ∨ ( 𝑏𝑤 ) = 1o ) )
80 71 76 79 mpjaodan ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) → ( ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) )
81 56 80 impbid2 ( ( ( 𝑏𝑤 ) ∈ 2o ∧ ( 𝑐𝑤 ) ∈ 2o ) → ( ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ↔ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) )
82 54 55 81 syl2anc ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ↔ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) )
83 simplrl ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → 𝑏 ∈ ( 2om 𝐴 ) )
84 3 pw2f1o2val2 ( ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑤𝐴 ) → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ ( 𝑏𝑤 ) = 1o ) )
85 83 84 sylancom ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ ( 𝑏𝑤 ) = 1o ) )
86 simplrr ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → 𝑐 ∈ ( 2om 𝐴 ) )
87 3 pw2f1o2val2 ( ( 𝑐 ∈ ( 2om 𝐴 ) ∧ 𝑤𝐴 ) → ( 𝑤 ∈ ( 𝐹𝑐 ) ↔ ( 𝑐𝑤 ) = 1o ) )
88 86 87 sylancom ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( 𝑤 ∈ ( 𝐹𝑐 ) ↔ ( 𝑐𝑤 ) = 1o ) )
89 85 88 bibi12d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ↔ ( ( 𝑏𝑤 ) = 1o ↔ ( 𝑐𝑤 ) = 1o ) ) )
90 82 89 bitr4d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ↔ ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) )
91 90 imbi2d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑤𝐴 ) → ( ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
92 91 ralbidva ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) → ( ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ↔ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
93 92 adantr ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ↔ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
94 53 93 anbi12d ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) ∧ 𝑧𝐴 ) → ( ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) ↔ ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) ) )
95 94 rexbidva ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) → ( ∃ 𝑧𝐴 ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) ↔ ∃ 𝑧𝐴 ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) ) )
96 vex 𝑏 ∈ V
97 vex 𝑐 ∈ V
98 fveq1 ( 𝑥 = 𝑏 → ( 𝑥𝑧 ) = ( 𝑏𝑧 ) )
99 fveq1 ( 𝑦 = 𝑐 → ( 𝑦𝑧 ) = ( 𝑐𝑧 ) )
100 98 99 breqan12d ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ↔ ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ) )
101 fveq1 ( 𝑥 = 𝑏 → ( 𝑥𝑤 ) = ( 𝑏𝑤 ) )
102 fveq1 ( 𝑦 = 𝑐 → ( 𝑦𝑤 ) = ( 𝑐𝑤 ) )
103 101 102 eqeqan12d ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ↔ ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) )
104 103 imbi2d ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) )
105 104 ralbidv ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) )
106 100 105 anbi12d ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) ) )
107 106 rexbidv ( ( 𝑥 = 𝑏𝑦 = 𝑐 ) → ( ∃ 𝑧𝐴 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑧𝐴 ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) ) )
108 96 97 107 2 braba ( 𝑏 𝑈 𝑐 ↔ ∃ 𝑧𝐴 ( ( 𝑏𝑧 ) E ( 𝑐𝑧 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏𝑤 ) = ( 𝑐𝑤 ) ) ) )
109 fvex ( 𝐹𝑏 ) ∈ V
110 fvex ( 𝐹𝑐 ) ∈ V
111 eleq2 ( 𝑦 = ( 𝐹𝑐 ) → ( 𝑧𝑦𝑧 ∈ ( 𝐹𝑐 ) ) )
112 eleq2 ( 𝑥 = ( 𝐹𝑏 ) → ( 𝑧𝑥𝑧 ∈ ( 𝐹𝑏 ) ) )
113 112 notbid ( 𝑥 = ( 𝐹𝑏 ) → ( ¬ 𝑧𝑥 ↔ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) )
114 111 113 bi2anan9r ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ( 𝑧𝑦 ∧ ¬ 𝑧𝑥 ) ↔ ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ) )
115 eleq2 ( 𝑥 = ( 𝐹𝑏 ) → ( 𝑤𝑥𝑤 ∈ ( 𝐹𝑏 ) ) )
116 eleq2 ( 𝑦 = ( 𝐹𝑐 ) → ( 𝑤𝑦𝑤 ∈ ( 𝐹𝑐 ) ) )
117 115 116 bi2bian9 ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ( 𝑤𝑥𝑤𝑦 ) ↔ ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) )
118 117 imbi2d ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
119 118 ralbidv ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ↔ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
120 114 119 anbi12d ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ( ( 𝑧𝑦 ∧ ¬ 𝑧𝑥 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ) ↔ ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) ) )
121 120 rexbidv ( ( 𝑥 = ( 𝐹𝑏 ) ∧ 𝑦 = ( 𝐹𝑐 ) ) → ( ∃ 𝑧𝐴 ( ( 𝑧𝑦 ∧ ¬ 𝑧𝑥 ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤𝑥𝑤𝑦 ) ) ) ↔ ∃ 𝑧𝐴 ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) ) )
122 109 110 121 1 braba ( ( 𝐹𝑏 ) 𝑇 ( 𝐹𝑐 ) ↔ ∃ 𝑧𝐴 ( ( 𝑧 ∈ ( 𝐹𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹𝑏 ) ) ∧ ∀ 𝑤𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹𝑏 ) ↔ 𝑤 ∈ ( 𝐹𝑐 ) ) ) ) )
123 95 108 122 3bitr4g ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2om 𝐴 ) ∧ 𝑐 ∈ ( 2om 𝐴 ) ) ) → ( 𝑏 𝑈 𝑐 ↔ ( 𝐹𝑏 ) 𝑇 ( 𝐹𝑐 ) ) )
124 123 ralrimivva ( 𝐴 ∈ V → ∀ 𝑏 ∈ ( 2om 𝐴 ) ∀ 𝑐 ∈ ( 2om 𝐴 ) ( 𝑏 𝑈 𝑐 ↔ ( 𝐹𝑏 ) 𝑇 ( 𝐹𝑐 ) ) )
125 df-isom ( 𝐹 Isom 𝑈 , 𝑇 ( ( 2om 𝐴 ) , 𝒫 𝐴 ) ↔ ( 𝐹 : ( 2om 𝐴 ) –1-1-onto→ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ( 2om 𝐴 ) ∀ 𝑐 ∈ ( 2om 𝐴 ) ( 𝑏 𝑈 𝑐 ↔ ( 𝐹𝑏 ) 𝑇 ( 𝐹𝑐 ) ) ) )
126 4 124 125 sylanbrc ( 𝐴 ∈ V → 𝐹 Isom 𝑈 , 𝑇 ( ( 2om 𝐴 ) , 𝒫 𝐴 ) )