Metamath Proof Explorer

Theorem tfsconcatrn

Description: The range of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025)

Ref Expression
Hypothesis tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
Assertion tfsconcatrn ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 1 tfsconcatun ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
3 2 rneqd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ran ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
4 rnun ⊢ ran ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = ( ran 𝐴 ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } )
5 4 a1i ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = ( ran 𝐴 ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
6 df-rex ⊢ ( ∃ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
7 pm3.22 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) )
8 7 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) )
9 oaordi ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑑 ∈ 𝐷 → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) )
10 8 9 syl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑑 ∈ 𝐷 → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) )
11 10 imp ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) )
12 simplrl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → 𝐶 ∈ On )
13 simprr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐷 ∈ On )
14 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ On )
15 13 14 sylan ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ On )
16 oaword1 ⊢ ( ( 𝐶 ∈ On ∧ 𝑑 ∈ On ) → 𝐶 ⊆ ( 𝐶 +o 𝑑 ) )
17 12 15 16 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → 𝐶 ⊆ ( 𝐶 +o 𝑑 ) )
18 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +o 𝐷 ) ∈ On )
19 18 ad2antlr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 +o 𝐷 ) ∈ On )
20 eloni ⊢ ( ( 𝐶 +o 𝐷 ) ∈ On → Ord ( 𝐶 +o 𝐷 ) )
21 19 20 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → Ord ( 𝐶 +o 𝐷 ) )
22 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
23 12 22 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → Ord 𝐶 )
24 ordeldif ⊢ ( ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) → ( ( 𝐶 +o 𝑑 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ ( 𝐶 +o 𝑑 ) ) ) )
25 21 23 24 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝐶 +o 𝑑 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ ( 𝐶 +o 𝑑 ) ) ) )
26 11 17 25 mpbir2and ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 +o 𝑑 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
27 simpr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
28 27 adantr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
29 18 20 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord ( 𝐶 +o 𝐷 ) )
30 22 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord 𝐶 )
31 29 30 jca ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
32 31 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
33 ordeldif ⊢ ( ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) ) )
34 32 33 syl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) ) )
35 34 biimpa ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) )
36 35 ancomd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) )
37 oawordex2 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) ) → ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑥 )
38 28 36 37 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑥 )
39 eqcom ⊢ ( ( 𝐶 +o 𝑑 ) = 𝑥 ↔ 𝑥 = ( 𝐶 +o 𝑑 ) )
40 39 rexbii ⊢ ( ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑥 ↔ ∃ 𝑑 ∈ 𝐷 𝑥 = ( 𝐶 +o 𝑑 ) )
41 38 40 sylib ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ∃ 𝑑 ∈ 𝐷 𝑥 = ( 𝐶 +o 𝑑 ) )
42 simpr ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → 𝑥 = ( 𝐶 +o 𝑧 ) )
43 simpll3 ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → 𝑥 = ( 𝐶 +o 𝑑 ) )
44 42 43 eqtr3d ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( 𝐶 +o 𝑧 ) = ( 𝐶 +o 𝑑 ) )
45 simp1rl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → 𝐶 ∈ On )
46 45 adantr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝐶 ∈ On )
47 simp1rr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → 𝐷 ∈ On )
48 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ On )
49 47 48 sylan ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ On )
50 simp2 ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → 𝑑 ∈ 𝐷 )
51 47 50 14 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → 𝑑 ∈ On )
52 51 adantr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑑 ∈ On )
53 46 49 52 3jca ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝐶 ∈ On ∧ 𝑧 ∈ On ∧ 𝑑 ∈ On ) )
54 53 adantr ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( 𝐶 ∈ On ∧ 𝑧 ∈ On ∧ 𝑑 ∈ On ) )
55 oacan ⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ On ∧ 𝑑 ∈ On ) → ( ( 𝐶 +o 𝑧 ) = ( 𝐶 +o 𝑑 ) ↔ 𝑧 = 𝑑 ) )
56 54 55 syl ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( ( 𝐶 +o 𝑧 ) = ( 𝐶 +o 𝑑 ) ↔ 𝑧 = 𝑑 ) )
57 44 56 mpbid ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → 𝑧 = 𝑑 )
58 velsn ⊢ ( 𝑧 ∈ { 𝑑 } ↔ 𝑧 = 𝑑 )
59 57 58 sylibr ⊢ ( ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → 𝑧 ∈ { 𝑑 } )
60 59 ex ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑥 = ( 𝐶 +o 𝑧 ) → 𝑧 ∈ { 𝑑 } ) )
61 60 adantrd ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) → 𝑧 ∈ { 𝑑 } ) )
62 61 expimpd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) → 𝑧 ∈ { 𝑑 } ) )
63 simprr ⊢ ( ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) → 𝑦 = ( 𝐵 ‘ 𝑧 ) )
64 62 63 jca2 ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) → ( 𝑧 ∈ { 𝑑 } ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
65 64 reximdv2 ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) → ∃ 𝑧 ∈ { 𝑑 } 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
66 vex ⊢ 𝑑 ∈ V
67 fveq2 ⊢ ( 𝑧 = 𝑑 → ( 𝐵 ‘ 𝑧 ) = ( 𝐵 ‘ 𝑑 ) )
68 67 eqeq2d ⊢ ( 𝑧 = 𝑑 → ( 𝑦 = ( 𝐵 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) )
69 66 68 rexsn ⊢ ( ∃ 𝑧 ∈ { 𝑑 } 𝑦 = ( 𝐵 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐵 ‘ 𝑑 ) )
70 65 69 imbitrdi ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) → 𝑦 = ( 𝐵 ‘ 𝑑 ) ) )
71 50 adantr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) → 𝑑 ∈ 𝐷 )
72 simpl3 ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) → 𝑥 = ( 𝐶 +o 𝑑 ) )
73 simpr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) → 𝑦 = ( 𝐵 ‘ 𝑑 ) )
74 oveq2 ⊢ ( 𝑧 = 𝑑 → ( 𝐶 +o 𝑧 ) = ( 𝐶 +o 𝑑 ) )
75 74 eqeq2d ⊢ ( 𝑧 = 𝑑 → ( 𝑥 = ( 𝐶 +o 𝑧 ) ↔ 𝑥 = ( 𝐶 +o 𝑑 ) ) )
76 75 68 anbi12d ⊢ ( 𝑧 = 𝑑 → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 = ( 𝐶 +o 𝑑 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) ) )
77 76 rspcev ⊢ ( ( 𝑑 ∈ 𝐷 ∧ ( 𝑥 = ( 𝐶 +o 𝑑 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
78 71 72 73 77 syl12anc ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) ∧ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
79 78 ex ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( 𝑦 = ( 𝐵 ‘ 𝑑 ) → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
80 70 79 impbid ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ∧ 𝑥 = ( 𝐶 +o 𝑑 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ 𝑦 = ( 𝐵 ‘ 𝑑 ) ) )
81 26 41 80 rexxfrd2 ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ∃ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑑 ∈ 𝐷 𝑦 = ( 𝐵 ‘ 𝑑 ) ) )
82 6 81 bitr3id ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ∃ 𝑥 ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ∃ 𝑑 ∈ 𝐷 𝑦 = ( 𝐵 ‘ 𝑑 ) ) )
83 82 abbidv ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { 𝑦 ∣ ∃ 𝑑 ∈ 𝐷 𝑦 = ( 𝐵 ‘ 𝑑 ) } )
84 rnopab ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) }
85 84 a1i ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } )
86 fnrnfv ⊢ ( 𝐵 Fn 𝐷 → ran 𝐵 = { 𝑦 ∣ ∃ 𝑑 ∈ 𝐷 𝑦 = ( 𝐵 ‘ 𝑑 ) } )
87 86 ad2antlr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran 𝐵 = { 𝑦 ∣ ∃ 𝑑 ∈ 𝐷 𝑦 = ( 𝐵 ‘ 𝑑 ) } )
88 83 85 87 3eqtr4d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = ran 𝐵 )
89 88 uneq2d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ran 𝐴 ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = ( ran 𝐴 ∪ ran 𝐵 ) )
90 3 5 89 3eqtrd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )