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 ⊢ 𝐹 = ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) )
Assertion wepwsolem ( 𝐴 ∈ V → 𝐹 Isom 𝑈 , 𝑇 ( ( 2o ↑m 𝐴 ) , 𝒫 𝐴 ) )

Proof

Step Hyp Ref Expression
1 wepwso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ) ) }
2 wepwso.u ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
3 wepwso.f ⊢ 𝐹 = ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) )
4 3 pw2f1o2 ⊢ ( 𝐴 ∈ V → 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 )
5 fvex ⊢ ( 𝑐 ‘ 𝑧 ) ∈ V
6 5 epeli ⊢ ( ( 𝑏 ‘ 𝑧 ) E ( 𝑐 ‘ 𝑧 ) ↔ ( 𝑏 ‘ 𝑧 ) ∈ ( 𝑐 ‘ 𝑧 ) )
7 elmapi ⊢ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) → 𝑏 : 𝐴 ⟶ 2o )
8 7 ad2antrl ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) → 𝑏 : 𝐴 ⟶ 2o )
9 8 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑏 ‘ 𝑧 ) ∈ 2o )
10 elmapi ⊢ ( 𝑐 ∈ ( 2o ↑m 𝐴 ) → 𝑐 : 𝐴 ⟶ 2o )
11 10 ad2antll ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) → 𝑐 : 𝐴 ⟶ 2o )
12 11 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑐 ‘ 𝑧 ) ∈ 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 ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑏 ‘ 𝑧 ) ∈ ( 𝑐 ‘ 𝑧 ) ↔ ( ( 𝑐 ‘ 𝑧 ) = 1o ∧ ¬ ( 𝑏 ‘ 𝑧 ) = 1o ) ) )
44 simplrr ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑐 ∈ ( 2o ↑m 𝐴 ) )
45 3 pw2f1o2val2 ⊢ ( ( 𝑐 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑧 ) = 1o ) )
46 44 45 sylancom ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑧 ) = 1o ) )
47 simplrl ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑏 ∈ ( 2o ↑m 𝐴 ) )
48 3 pw2f1o2val2 ⊢ ( ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑏 ‘ 𝑧 ) = 1o ) )
49 47 48 sylancom ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑏 ‘ 𝑧 ) = 1o ) )
50 49 notbid ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ↔ ¬ ( 𝑏 ‘ 𝑧 ) = 1o ) )
51 46 50 anbi12d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝑐 ‘ 𝑧 ) = 1o ∧ ¬ ( 𝑏 ‘ 𝑧 ) = 1o ) ) )
52 43 51 bitr4d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑏 ‘ 𝑧 ) ∈ ( 𝑐 ‘ 𝑧 ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ) ) )
53 6 52 bitrid ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑏 ‘ 𝑧 ) E ( 𝑐 ‘ 𝑧 ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ) ) )
54 8 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑏 ‘ 𝑤 ) ∈ 2o )
55 11 ffvelcdmda ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑐 ‘ 𝑤 ) ∈ 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 ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ↔ ( ( 𝑏 ‘ 𝑤 ) = 1o ↔ ( 𝑐 ‘ 𝑤 ) = 1o ) ) )
83 simplrl ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑏 ∈ ( 2o ↑m 𝐴 ) )
84 3 pw2f1o2val2 ⊢ ( ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑏 ‘ 𝑤 ) = 1o ) )
85 83 84 sylancom ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑏 ‘ 𝑤 ) = 1o ) )
86 simplrr ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑐 ∈ ( 2o ↑m 𝐴 ) )
87 3 pw2f1o2val2 ⊢ ( ( 𝑐 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑤 ) = 1o ) )
88 86 87 sylancom ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ↔ ( 𝑐 ‘ 𝑤 ) = 1o ) )
89 85 88 bibi12d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( 𝑏 ‘ 𝑤 ) = 1o ↔ ( 𝑐 ‘ 𝑤 ) = 1o ) ) )
90 82 89 bitr4d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ↔ ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ) )
91 90 imbi2d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑤 𝑅 𝑧 → ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ) ) )
92 91 ralbidva ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ) ) )
93 92 adantr ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ) ) )
94 53 93 anbi12d ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑏 ‘ 𝑧 ) E ( 𝑐 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑏 ‘ 𝑤 ) = ( 𝑐 ‘ 𝑤 ) ) ) ↔ ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑐 ) ∧ ¬ 𝑧 ∈ ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ ( 𝐹 ‘ 𝑏 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
95 94 rexbidva ⊢ ( ( 𝐴 ∈ V ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑏 ‘ 𝑧 ) 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 ∧ ( 𝑏 ∈ ( 2o ↑m 𝐴 ) ∧ 𝑐 ∈ ( 2o ↑m 𝐴 ) ) ) → ( 𝑏 𝑈 𝑐 ↔ ( 𝐹 ‘ 𝑏 ) 𝑇 ( 𝐹 ‘ 𝑐 ) ) )
124 123 ralrimivva ⊢ ( 𝐴 ∈ V → ∀ 𝑏 ∈ ( 2o ↑m 𝐴 ) ∀ 𝑐 ∈ ( 2o ↑m 𝐴 ) ( 𝑏 𝑈 𝑐 ↔ ( 𝐹 ‘ 𝑏 ) 𝑇 ( 𝐹 ‘ 𝑐 ) ) )
125 df-isom ⊢ ( 𝐹 Isom 𝑈 , 𝑇 ( ( 2o ↑m 𝐴 ) , 𝒫 𝐴 ) ↔ ( 𝐹 : ( 2o ↑m 𝐴 ) –1-1-onto→ 𝒫 𝐴 ∧ ∀ 𝑏 ∈ ( 2o ↑m 𝐴 ) ∀ 𝑐 ∈ ( 2o ↑m 𝐴 ) ( 𝑏 𝑈 𝑐 ↔ ( 𝐹 ‘ 𝑏 ) 𝑇 ( 𝐹 ‘ 𝑐 ) ) ) )
126 4 124 125 sylanbrc ⊢ ( 𝐴 ∈ V → 𝐹 Isom 𝑈 , 𝑇 ( ( 2o ↑m 𝐴 ) , 𝒫 𝐴 ) )