Metamath Proof Explorer

Theorem tfsconcatlem

Description: Lemma for tfsconcatun . (Contributed by RP, 23-Feb-2025)

Ref Expression
Assertion tfsconcatlem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ( 𝐴 +o 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
2 1 3ad2ant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → 𝐵 ⊆ On )
3 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
4 eloni ⊢ ( ( 𝐴 +o 𝐵 ) ∈ On → Ord ( 𝐴 +o 𝐵 ) )
5 3 4 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 +o 𝐵 ) )
6 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
7 6 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord 𝐴 )
8 ordeldif ⊢ ( ( Ord ( 𝐴 +o 𝐵 ) ∧ Ord 𝐴 ) → ( 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐶 ∈ ( 𝐴 +o 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) ) )
9 5 7 8 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ↔ ( 𝐶 ∈ ( 𝐴 +o 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) ) )
10 9 biimpa ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( 𝐶 ∈ ( 𝐴 +o 𝐵 ) ∧ 𝐴 ⊆ 𝐶 ) )
11 10 ancomd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) )
12 11 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) ) )
13 12 imdistani ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) ) )
14 13 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) ) )
15 oawordex2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 +o 𝐵 ) ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
16 14 15 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
17 simp1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → 𝐴 ∈ On )
18 onss ⊢ ( ( 𝐴 +o 𝐵 ) ∈ On → ( 𝐴 +o 𝐵 ) ⊆ On )
19 3 18 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ⊆ On )
20 19 ssdifd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ⊆ ( On ∖ 𝐴 ) )
21 20 sselda ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → 𝐶 ∈ ( On ∖ 𝐴 ) )
22 21 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → 𝐶 ∈ ( On ∖ 𝐴 ) )
23 ordon ⊢ Ord On
24 17 6 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → Ord 𝐴 )
25 ordeldif ⊢ ( ( Ord On ∧ Ord 𝐴 ) → ( 𝐶 ∈ ( On ∖ 𝐴 ) ↔ ( 𝐶 ∈ On ∧ 𝐴 ⊆ 𝐶 ) ) )
26 23 24 25 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( 𝐶 ∈ ( On ∖ 𝐴 ) ↔ ( 𝐶 ∈ On ∧ 𝐴 ⊆ 𝐶 ) ) )
27 22 26 mpbid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( 𝐶 ∈ On ∧ 𝐴 ⊆ 𝐶 ) )
28 anass ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐶 ) ↔ ( 𝐴 ∈ On ∧ ( 𝐶 ∈ On ∧ 𝐴 ⊆ 𝐶 ) ) )
29 17 27 28 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐶 ) )
30 oawordeu ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝐴 ⊆ 𝐶 ) → ∃! 𝑦 ∈ On ( 𝐴 +o 𝑦 ) = 𝐶 )
31 29 30 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃! 𝑦 ∈ On ( 𝐴 +o 𝑦 ) = 𝐶 )
32 reuss ⊢ ( ( 𝐵 ⊆ On ∧ ∃ 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃! 𝑦 ∈ On ( 𝐴 +o 𝑦 ) = 𝐶 ) → ∃! 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
33 2 16 31 32 syl3anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃! 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
34 reurmo ⊢ ( ∃! 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 → ∃* 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
35 33 34 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃* 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 )
36 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) )
37 35 36 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) )
38 moeq ⊢ ∃* 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 )
39 38 ax-gen ⊢ ∀ 𝑦 ∃* 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 )
40 moexexvw ⊢ ( ( ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ ∀ 𝑦 ∃* 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ∃* 𝑥 ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
41 37 39 40 sylancl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃* 𝑥 ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
42 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
43 anass ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
44 43 exbii ⊢ ( ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
45 42 44 bitr4i ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
46 45 mobii ⊢ ( ∃* 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃* 𝑥 ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ ( 𝐴 +o 𝑦 ) = 𝐶 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
47 41 46 sylibr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃* 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
48 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
49 48 isseti ⊢ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 )
50 49 jctr ⊢ ( ( 𝐴 +o 𝑦 ) = 𝐶 → ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
51 50 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 +o 𝑦 ) = 𝐶 → ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
52 51 reximdva ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝐴 +o 𝑦 ) = 𝐶 → ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
53 16 52 mpd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
54 rexcom4a ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
55 exmoeu ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∃* 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
56 54 55 bitr3i ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ ∃ 𝑥 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∃* 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
57 53 56 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ( ∃* 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ) )
58 47 57 mpd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
59 eqcom ⊢ ( ( 𝐴 +o 𝑦 ) = 𝐶 ↔ 𝐶 = ( 𝐴 +o 𝑦 ) )
60 59 anbi1i ⊢ ( ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐶 = ( 𝐴 +o 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
61 60 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ( 𝐴 +o 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
62 61 eubii ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( ( 𝐴 +o 𝑦 ) = 𝐶 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) ↔ ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ( 𝐴 +o 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
63 58 62 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) → ∃! 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ( 𝐴 +o 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )