Metamath Proof Explorer

Theorem onprcf1of1ord

Description: If F is a bijection from the ordinals to the universe, H is a bijection from the ordinals to A if A is a proper class, and I is a bijection from the ordinals to B if B is a proper class, then J either maps A one-to-one into B or maps B one-to-one into A . This is the ZFC version of (5 -> 10) in https://tinyurl.com/hamkins-gblac . Note that in NBG set theory the first three hypotheses would be replaced by something like ( ph -> A. X ( -. X e. _V -> E. F F : On -1-1-onto-> X ) ) . However, we cannot quantify over classes, so we split this into the case where X is the universe, the case where X is an arbitrary proper class A , and the case where X is an arbitrary proper class B , which together are sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026)

Ref Expression
Hypotheses onprcf1of1ord.1 ⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )
onprcf1of1ord.2 ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ V → 𝐻 : On –1-1-onto→ 𝐴 ) )
onprcf1of1ord.3 ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ V → 𝐼 : On –1-1-onto→ 𝐵 ) )
onprcf1of1ord.4 ⊢ 𝐽 = if ( 𝐴 ∈ V , if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) , ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) )
onprcf1of1ord.5 ⊢ 𝐾 = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } )
Assertion onprcf1of1ord ( 𝜑 → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 onprcf1of1ord.1 ⊢ ( 𝜑 → 𝐹 : On –1-1-onto→ V )
2 onprcf1of1ord.2 ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ V → 𝐻 : On –1-1-onto→ 𝐴 ) )
3 onprcf1of1ord.3 ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ V → 𝐼 : On –1-1-onto→ 𝐵 ) )
4 onprcf1of1ord.4 ⊢ 𝐽 = if ( 𝐴 ∈ V , if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) , ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) )
5 onprcf1of1ord.5 ⊢ 𝐾 = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } )
6 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐹 : On –1-1-onto→ V )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
9 6 7 8 onprcf1of1orbd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∨ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 ) )
10 19.43 ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ∨ ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐴 ) )
11 9 10 sylibr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) )
12 dff1o5 ⊢ ( 𝐹 : On –1-1-onto→ V ↔ ( 𝐹 : On –1-1→ V ∧ ran 𝐹 = V ) )
13 12 simprbi ⊢ ( 𝐹 : On –1-1-onto→ V → ran 𝐹 = V )
14 1 13 syl ⊢ ( 𝜑 → ran 𝐹 = V )
15 14 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ran 𝐹 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑓 ∈ V ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ) )
16 rexv ⊢ ( ∃ 𝑓 ∈ V ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) )
17 15 16 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ran 𝐹 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ) )
18 f1ofn ⊢ ( 𝐹 : On –1-1-onto→ V → 𝐹 Fn On )
19 f1eq1 ⊢ ( 𝑓 = ( 𝐹 ‘ 𝑥 ) → ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ) )
20 f1eq1 ⊢ ( 𝑓 = ( 𝐹 ‘ 𝑥 ) → ( 𝑓 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) )
21 19 20 orbi12d ⊢ ( 𝑓 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ) )
22 21 rexrn ⊢ ( 𝐹 Fn On → ( ∃ 𝑓 ∈ ran 𝐹 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ) )
23 1 18 22 3syl ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ran 𝐹 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ) )
24 17 23 bitr3d ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 –1-1→ 𝐵 ∨ 𝑓 : 𝐵 –1-1→ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ) )
26 11 25 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) )
27 nfcv ⊢ Ⅎ 𝑥 𝐹
28 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) }
29 28 nfint ⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) }
30 27 29 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } )
31 nfcv ⊢ Ⅎ 𝑥 𝐴
32 nfcv ⊢ Ⅎ 𝑥 𝐵
33 30 31 32 nff1 ⊢ Ⅎ 𝑥 ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵
34 30 32 31 nff1 ⊢ Ⅎ 𝑥 ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴
35 33 34 nfor ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 )
36 fveq2 ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) )
37 f1eq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) → ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ) )
38 36 37 syl ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } → ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ) )
39 f1eq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) → ( ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
40 36 39 syl ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } → ( ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
41 38 40 orbi12d ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } → ( ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) ↔ ( ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) ) )
42 35 41 onminsb ⊢ ( ∃ 𝑥 ∈ On ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) → ( ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
43 26 42 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
44 iftrue ⊢ ( 𝐴 ∈ V → if ( 𝐴 ∈ V , if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) , ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) ) = if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) )
45 4 44 eqtrid ⊢ ( 𝐴 ∈ V → 𝐽 = if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐽 = if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) )
47 iftrue ⊢ ( 𝐵 ∈ V → if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) = 𝐾 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) = 𝐾 )
49 46 48 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐽 = 𝐾 )
50 49 5 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → 𝐽 = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) )
51 f1eq1 ⊢ ( 𝐽 = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ) )
52 50 51 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ) )
53 f1eq1 ⊢ ( 𝐽 = ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) → ( 𝐽 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
54 50 53 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( 𝐽 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) )
55 52 54 orbi12d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) ↔ ( ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ ∩ { 𝑥 ∈ On ∣ ( ( 𝐹 ‘ 𝑥 ) : 𝐴 –1-1→ 𝐵 ∨ ( 𝐹 ‘ 𝑥 ) : 𝐵 –1-1→ 𝐴 ) } ) : 𝐵 –1-1→ 𝐴 ) ) )
56 43 55 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝐵 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )
57 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → 𝐹 : On –1-1-onto→ V )
58 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → ( ¬ 𝐵 ∈ V → 𝐼 : On –1-1-onto→ 𝐵 ) )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → ¬ 𝐵 ∈ V )
60 eqid ⊢ ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) = ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) )
61 57 58 59 60 onprcf1of1orad ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 )
62 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → 𝐽 = if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) )
63 iffalse ⊢ ( ¬ 𝐵 ∈ V → if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) = ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) = ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) )
65 62 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → 𝐽 = ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) )
66 f1eq1 ⊢ ( 𝐽 = ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) )
67 65 66 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) : 𝐴 –1-1→ 𝐵 ) )
68 61 67 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → 𝐽 : 𝐴 –1-1→ 𝐵 )
69 68 orcd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ ¬ 𝐵 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )
70 56 69 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )
71 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → 𝐹 : On –1-1-onto→ V )
72 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → ( ¬ 𝐴 ∈ V → 𝐻 : On –1-1-onto→ 𝐴 ) )
73 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 ∈ V )
74 eqid ⊢ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) )
75 71 72 73 74 onprcf1of1orad ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) : 𝐵 –1-1→ 𝐴 )
76 iffalse ⊢ ( ¬ 𝐴 ∈ V → if ( 𝐴 ∈ V , if ( 𝐵 ∈ V , 𝐾 , ( 𝐼 ∘ ( ◡ 𝐹 ↾ 𝐴 ) ) ) , ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) ) = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) )
77 4 76 eqtrid ⊢ ( ¬ 𝐴 ∈ V → 𝐽 = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) )
78 f1eq1 ⊢ ( 𝐽 = ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) → ( 𝐽 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) : 𝐵 –1-1→ 𝐴 ) )
79 77 78 syl ⊢ ( ¬ 𝐴 ∈ V → ( 𝐽 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) : 𝐵 –1-1→ 𝐴 ) )
80 79 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → ( 𝐽 : 𝐵 –1-1→ 𝐴 ↔ ( 𝐻 ∘ ( ◡ 𝐹 ↾ 𝐵 ) ) : 𝐵 –1-1→ 𝐴 ) )
81 75 80 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → 𝐽 : 𝐵 –1-1→ 𝐴 )
82 81 olcd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ V ) → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )
83 70 82 pm2.61dan ⊢ ( 𝜑 → ( 𝐽 : 𝐴 –1-1→ 𝐵 ∨ 𝐽 : 𝐵 –1-1→ 𝐴 ) )