Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tfsconcatrev Structured version   Visualization version   GIF version
Theorem tfsconcatrev 42401
Description: If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.)
Hypothesis
Ref Expression
tfsconcat.op + = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ž βˆͺ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((dom π‘Ž +o dom 𝑏) βˆ– dom π‘Ž) ∧ βˆƒπ‘§ ∈ dom 𝑏(π‘₯ = (dom π‘Ž +o 𝑧) ∧ 𝑦 = (π‘β€˜π‘§)))}))
Assertion
Ref Expression
tfsconcatrev ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ βˆƒπ‘’ ∈ (ran 𝐹 ↑m 𝐢)βˆƒπ‘£ ∈ (ran 𝐹 ↑m 𝐷)((𝑒 + 𝑣) = 𝐹 ∧ dom 𝑒 = 𝐢 ∧ dom 𝑣 = 𝐷))
Distinct variable groups:   π‘Ž,𝑏,𝑒,𝑣,π‘₯,𝑦,𝑧,𝐢   𝐷,π‘Ž,𝑏,𝑒,𝑣,π‘₯,𝑦,𝑧   𝐹,π‘Ž,𝑏,𝑒,𝑣,π‘₯,𝑦,𝑧   𝑒, + ,𝑣
Allowed substitution hints:   + (π‘₯,𝑦,𝑧,π‘Ž,𝑏)
Proof of Theorem tfsconcatrev
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 dffn3 6731 . . . . . 6 (𝐹 Fn (𝐢 +o 𝐷) ↔ 𝐹:(𝐢 +o 𝐷)⟢ran 𝐹)
21biimpi 215 . . . . 5 (𝐹 Fn (𝐢 +o 𝐷) β†’ 𝐹:(𝐢 +o 𝐷)⟢ran 𝐹)
32adantr 480 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐹:(𝐢 +o 𝐷)⟢ran 𝐹)
4 fndm 6653 . . . . . . . 8 (𝐹 Fn (𝐢 +o 𝐷) β†’ dom 𝐹 = (𝐢 +o 𝐷))
54adantr 480 . . . . . . 7 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ dom 𝐹 = (𝐢 +o 𝐷))
6 oacl 8538 . . . . . . . 8 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ (𝐢 +o 𝐷) ∈ On)
76adantl 481 . . . . . . 7 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐢 +o 𝐷) ∈ On)
85, 7eqeltrd 2832 . . . . . 6 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ dom 𝐹 ∈ On)
9 fnfun 6650 . . . . . . 7 (𝐹 Fn (𝐢 +o 𝐷) β†’ Fun 𝐹)
109adantr 480 . . . . . 6 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ Fun 𝐹)
11 funrnex 7943 . . . . . 6 (dom 𝐹 ∈ On β†’ (Fun 𝐹 β†’ ran 𝐹 ∈ V))
128, 10, 11sylc 65 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ran 𝐹 ∈ V)
1312, 7elmapd 8837 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 ∈ (ran 𝐹 ↑m (𝐢 +o 𝐷)) ↔ 𝐹:(𝐢 +o 𝐷)⟢ran 𝐹))
143, 13mpbird 256 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐹 ∈ (ran 𝐹 ↑m (𝐢 +o 𝐷)))
15 oaword1 8555 . . . 4 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ 𝐢 βŠ† (𝐢 +o 𝐷))
1615adantl 481 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐢 βŠ† (𝐢 +o 𝐷))
17 elmapssres 8864 . . 3 ((𝐹 ∈ (ran 𝐹 ↑m (𝐢 +o 𝐷)) ∧ 𝐢 βŠ† (𝐢 +o 𝐷)) β†’ (𝐹 β†Ύ 𝐢) ∈ (ran 𝐹 ↑m 𝐢))
1814, 16, 17syl2anc 583 . 2 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ 𝐢) ∈ (ran 𝐹 ↑m 𝐢))
19 simpl 482 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐹 Fn (𝐢 +o 𝐷))
20 oaordi 8549 . . . . . . . 8 ((𝐷 ∈ On ∧ 𝐢 ∈ On) β†’ (𝑑 ∈ 𝐷 β†’ (𝐢 +o 𝑑) ∈ (𝐢 +o 𝐷)))
2120ancoms 458 . . . . . . 7 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ (𝑑 ∈ 𝐷 β†’ (𝐢 +o 𝑑) ∈ (𝐢 +o 𝐷)))
2221adantl 481 . . . . . 6 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝑑 ∈ 𝐷 β†’ (𝐢 +o 𝑑) ∈ (𝐢 +o 𝐷)))
2322imp 406 . . . . 5 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑑 ∈ 𝐷) β†’ (𝐢 +o 𝑑) ∈ (𝐢 +o 𝐷))
24 fnfvelrn 7083 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 +o 𝑑) ∈ (𝐢 +o 𝐷)) β†’ (πΉβ€˜(𝐢 +o 𝑑)) ∈ ran 𝐹)
2519, 23, 24syl2an2r 682 . . . 4 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜(𝐢 +o 𝑑)) ∈ ran 𝐹)
2625fmpttd 7117 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))):𝐷⟢ran 𝐹)
27 simprr 770 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐷 ∈ On)
2812, 27elmapd 8837 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) ∈ (ran 𝐹 ↑m 𝐷) ↔ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))):𝐷⟢ran 𝐹))
2926, 28mpbird 256 . 2 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) ∈ (ran 𝐹 ↑m 𝐷))
3019, 16fnssresd 6675 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ 𝐢) Fn 𝐢)
31 fvex 6905 . . . . . . 7 (πΉβ€˜(𝐢 +o 𝑑)) ∈ V
32 eqid 2731 . . . . . . 7 (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))
3331, 32fnmpti 6694 . . . . . 6 (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) Fn 𝐷
3433a1i 11 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) Fn 𝐷)
35 simpr 484 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐢 ∈ On ∧ 𝐷 ∈ On))
36 tfsconcat.op . . . . . 6 + = (π‘Ž ∈ V, 𝑏 ∈ V ↦ (π‘Ž βˆͺ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((dom π‘Ž +o dom 𝑏) βˆ– dom π‘Ž) ∧ βˆƒπ‘§ ∈ dom 𝑏(π‘₯ = (dom π‘Ž +o 𝑧) ∧ 𝑦 = (π‘β€˜π‘§)))}))
3736tfsconcatun 42390 . . . . 5 ((((𝐹 β†Ύ 𝐢) Fn 𝐢 ∧ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) Fn 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = ((𝐹 β†Ύ 𝐢) βˆͺ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))}))
3830, 34, 35, 37syl21anc 835 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = ((𝐹 β†Ύ 𝐢) βˆͺ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))}))
39 oveq2 7420 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑧 β†’ (𝐢 +o 𝑑) = (𝐢 +o 𝑧))
4039fveq2d 6896 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑧 β†’ (πΉβ€˜(𝐢 +o 𝑑)) = (πΉβ€˜(𝐢 +o 𝑧)))
41 fvex 6905 . . . . . . . . . . . . . . . . 17 (πΉβ€˜(𝐢 +o 𝑧)) ∈ V
4240, 32, 41fvmpt 6999 . . . . . . . . . . . . . . . 16 (𝑧 ∈ 𝐷 β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) = (πΉβ€˜(𝐢 +o 𝑧)))
4342ad2antlr 724 . . . . . . . . . . . . . . 15 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) ∧ π‘₯ = (𝐢 +o 𝑧)) β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) = (πΉβ€˜(𝐢 +o 𝑧)))
44 fveq2 6892 . . . . . . . . . . . . . . . 16 (π‘₯ = (𝐢 +o 𝑧) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(𝐢 +o 𝑧)))
4544adantl 481 . . . . . . . . . . . . . . 15 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) ∧ π‘₯ = (𝐢 +o 𝑧)) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(𝐢 +o 𝑧)))
4643, 45eqtr4d 2774 . . . . . . . . . . . . . 14 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) ∧ π‘₯ = (𝐢 +o 𝑧)) β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) = (πΉβ€˜π‘₯))
4746eqeq2d 2742 . . . . . . . . . . . . 13 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) ∧ π‘₯ = (𝐢 +o 𝑧)) β†’ (𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) ↔ 𝑦 = (πΉβ€˜π‘₯)))
4847biimpd 228 . . . . . . . . . . . 12 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) ∧ π‘₯ = (𝐢 +o 𝑧)) β†’ (𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) β†’ 𝑦 = (πΉβ€˜π‘₯)))
4948expimpd 453 . . . . . . . . . . 11 ((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑧 ∈ 𝐷) β†’ ((π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)) β†’ 𝑦 = (πΉβ€˜π‘₯)))
5049rexlimdva 3154 . . . . . . . . . 10 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)) β†’ 𝑦 = (πΉβ€˜π‘₯)))
51 simplr 766 . . . . . . . . . . . . . . 15 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (𝐢 ∈ On ∧ 𝐷 ∈ On))
52 eloni 6375 . . . . . . . . . . . . . . . . . . . 20 ((𝐢 +o 𝐷) ∈ On β†’ Ord (𝐢 +o 𝐷))
536, 52syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ Ord (𝐢 +o 𝐷))
54 eloni 6375 . . . . . . . . . . . . . . . . . . . 20 (𝐢 ∈ On β†’ Ord 𝐢)
5554adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ Ord 𝐢)
56 ordeldif 42311 . . . . . . . . . . . . . . . . . . 19 ((Ord (𝐢 +o 𝐷) ∧ Ord 𝐢) β†’ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ↔ (π‘₯ ∈ (𝐢 +o 𝐷) ∧ 𝐢 βŠ† π‘₯)))
5753, 55, 56syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ↔ (π‘₯ ∈ (𝐢 +o 𝐷) ∧ 𝐢 βŠ† π‘₯)))
5857adantl 481 . . . . . . . . . . . . . . . . 17 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ↔ (π‘₯ ∈ (𝐢 +o 𝐷) ∧ 𝐢 βŠ† π‘₯)))
5958biimpa 476 . . . . . . . . . . . . . . . 16 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (π‘₯ ∈ (𝐢 +o 𝐷) ∧ 𝐢 βŠ† π‘₯))
6059ancomd 461 . . . . . . . . . . . . . . 15 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (𝐢 βŠ† π‘₯ ∧ π‘₯ ∈ (𝐢 +o 𝐷)))
6151, 60jca 511 . . . . . . . . . . . . . 14 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ ((𝐢 ∈ On ∧ 𝐷 ∈ On) ∧ (𝐢 βŠ† π‘₯ ∧ π‘₯ ∈ (𝐢 +o 𝐷))))
6261adantr 480 . . . . . . . . . . . . 13 ((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) β†’ ((𝐢 ∈ On ∧ 𝐷 ∈ On) ∧ (𝐢 βŠ† π‘₯ ∧ π‘₯ ∈ (𝐢 +o 𝐷))))
63 oawordex2 42379 . . . . . . . . . . . . 13 (((𝐢 ∈ On ∧ 𝐷 ∈ On) ∧ (𝐢 βŠ† π‘₯ ∧ π‘₯ ∈ (𝐢 +o 𝐷))) β†’ βˆƒπ‘§ ∈ 𝐷 (𝐢 +o 𝑧) = π‘₯)
6462, 63syl 17 . . . . . . . . . . . 12 ((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) β†’ βˆƒπ‘§ ∈ 𝐷 (𝐢 +o 𝑧) = π‘₯)
65 simpr 484 . . . . . . . . . . . . . . . 16 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ (𝐢 +o 𝑧) = π‘₯)
6665eqcomd 2737 . . . . . . . . . . . . . . 15 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ π‘₯ = (𝐢 +o 𝑧))
6765fveq2d 6896 . . . . . . . . . . . . . . . 16 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ (πΉβ€˜(𝐢 +o 𝑧)) = (πΉβ€˜π‘₯))
6842ad2antlr 724 . . . . . . . . . . . . . . . 16 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§) = (πΉβ€˜(𝐢 +o 𝑧)))
69 simpllr 773 . . . . . . . . . . . . . . . 16 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ 𝑦 = (πΉβ€˜π‘₯))
7067, 68, 693eqtr4rd 2782 . . . . . . . . . . . . . . 15 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§))
7166, 70jca 511 . . . . . . . . . . . . . 14 ((((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) ∧ (𝐢 +o 𝑧) = π‘₯) β†’ (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))
7271ex 412 . . . . . . . . . . . . 13 (((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) ∧ 𝑧 ∈ 𝐷) β†’ ((𝐢 +o 𝑧) = π‘₯ β†’ (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§))))
7372reximdva 3167 . . . . . . . . . . . 12 ((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) β†’ (βˆƒπ‘§ ∈ 𝐷 (𝐢 +o 𝑧) = π‘₯ β†’ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§))))
7464, 73mpd 15 . . . . . . . . . . 11 ((((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) ∧ 𝑦 = (πΉβ€˜π‘₯)) β†’ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))
7574ex 412 . . . . . . . . . 10 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (𝑦 = (πΉβ€˜π‘₯) β†’ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§))))
7650, 75impbid 211 . . . . . . . . 9 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)) ↔ 𝑦 = (πΉβ€˜π‘₯)))
77 eldifi 4127 . . . . . . . . . 10 (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) β†’ π‘₯ ∈ (𝐢 +o 𝐷))
78 eqcom 2738 . . . . . . . . . . 11 (𝑦 = (πΉβ€˜π‘₯) ↔ (πΉβ€˜π‘₯) = 𝑦)
79 fnbrfvb 6945 . . . . . . . . . . 11 ((𝐹 Fn (𝐢 +o 𝐷) ∧ π‘₯ ∈ (𝐢 +o 𝐷)) β†’ ((πΉβ€˜π‘₯) = 𝑦 ↔ π‘₯𝐹𝑦))
8078, 79bitrid 282 . . . . . . . . . 10 ((𝐹 Fn (𝐢 +o 𝐷) ∧ π‘₯ ∈ (𝐢 +o 𝐷)) β†’ (𝑦 = (πΉβ€˜π‘₯) ↔ π‘₯𝐹𝑦))
8119, 77, 80syl2an 595 . . . . . . . . 9 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (𝑦 = (πΉβ€˜π‘₯) ↔ π‘₯𝐹𝑦))
8276, 81bitrd 278 . . . . . . . 8 (((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) ∧ π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢)) β†’ (βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)) ↔ π‘₯𝐹𝑦))
8382pm5.32da 578 . . . . . . 7 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§))) ↔ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ π‘₯𝐹𝑦)))
8483opabbidv 5215 . . . . . 6 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))} = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ π‘₯𝐹𝑦)})
85 dfres2 6042 . . . . . 6 (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢)) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ π‘₯𝐹𝑦)}
8684, 85eqtr4di 2789 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))} = (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢)))
8786uneq2d 4164 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝐹 β†Ύ 𝐢) βˆͺ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ((𝐢 +o 𝐷) βˆ– 𝐢) ∧ βˆƒπ‘§ ∈ 𝐷 (π‘₯ = (𝐢 +o 𝑧) ∧ 𝑦 = ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))β€˜π‘§)))}) = ((𝐹 β†Ύ 𝐢) βˆͺ (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢))))
8838, 87eqtrd 2771 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = ((𝐹 β†Ύ 𝐢) βˆͺ (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢))))
89 resundi 5996 . . . 4 (𝐹 β†Ύ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢))) = ((𝐹 β†Ύ 𝐢) βˆͺ (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢)))
9089a1i 11 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢))) = ((𝐹 β†Ύ 𝐢) βˆͺ (𝐹 β†Ύ ((𝐢 +o 𝐷) βˆ– 𝐢))))
91 undif 4482 . . . . . . 7 (𝐢 βŠ† (𝐢 +o 𝐷) ↔ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢)) = (𝐢 +o 𝐷))
9215, 91sylib 217 . . . . . 6 ((𝐢 ∈ On ∧ 𝐷 ∈ On) β†’ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢)) = (𝐢 +o 𝐷))
9392adantl 481 . . . . 5 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢)) = (𝐢 +o 𝐷))
9493reseq2d 5982 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢))) = (𝐹 β†Ύ (𝐢 +o 𝐷)))
95 fnresdm 6670 . . . . 5 (𝐹 Fn (𝐢 +o 𝐷) β†’ (𝐹 β†Ύ (𝐢 +o 𝐷)) = 𝐹)
9695adantr 480 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ (𝐢 +o 𝐷)) = 𝐹)
9794, 96eqtrd 2771 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐹 β†Ύ (𝐢 βˆͺ ((𝐢 +o 𝐷) βˆ– 𝐢))) = 𝐹)
9888, 90, 973eqtr2d 2777 . 2 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = 𝐹)
99 dmres 6004 . . 3 dom (𝐹 β†Ύ 𝐢) = (𝐢 ∩ dom 𝐹)
10016, 5sseqtrrd 4024 . . . 4 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ 𝐢 βŠ† dom 𝐹)
101 df-ss 3966 . . . 4 (𝐢 βŠ† dom 𝐹 ↔ (𝐢 ∩ dom 𝐹) = 𝐢)
102100, 101sylib 217 . . 3 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ (𝐢 ∩ dom 𝐹) = 𝐢)
10399, 102eqtrid 2783 . 2 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ dom (𝐹 β†Ύ 𝐢) = 𝐢)
10431, 32dmmpti 6695 . . 3 dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = 𝐷
105104a1i 11 . 2 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = 𝐷)
106 oveq1 7419 . . . . 5 (𝑒 = (𝐹 β†Ύ 𝐢) β†’ (𝑒 + 𝑣) = ((𝐹 β†Ύ 𝐢) + 𝑣))
107106eqeq1d 2733 . . . 4 (𝑒 = (𝐹 β†Ύ 𝐢) β†’ ((𝑒 + 𝑣) = 𝐹 ↔ ((𝐹 β†Ύ 𝐢) + 𝑣) = 𝐹))
108 dmeq 5904 . . . . 5 (𝑒 = (𝐹 β†Ύ 𝐢) β†’ dom 𝑒 = dom (𝐹 β†Ύ 𝐢))
109108eqeq1d 2733 . . . 4 (𝑒 = (𝐹 β†Ύ 𝐢) β†’ (dom 𝑒 = 𝐢 ↔ dom (𝐹 β†Ύ 𝐢) = 𝐢))
110107, 1093anbi12d 1436 . . 3 (𝑒 = (𝐹 β†Ύ 𝐢) β†’ (((𝑒 + 𝑣) = 𝐹 ∧ dom 𝑒 = 𝐢 ∧ dom 𝑣 = 𝐷) ↔ (((𝐹 β†Ύ 𝐢) + 𝑣) = 𝐹 ∧ dom (𝐹 β†Ύ 𝐢) = 𝐢 ∧ dom 𝑣 = 𝐷)))
111 oveq2 7420 . . . . 5 (𝑣 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) β†’ ((𝐹 β†Ύ 𝐢) + 𝑣) = ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))))
112111eqeq1d 2733 . . . 4 (𝑣 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) β†’ (((𝐹 β†Ύ 𝐢) + 𝑣) = 𝐹 ↔ ((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = 𝐹))
113 dmeq 5904 . . . . 5 (𝑣 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) β†’ dom 𝑣 = dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))))
114113eqeq1d 2733 . . . 4 (𝑣 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) β†’ (dom 𝑣 = 𝐷 ↔ dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = 𝐷))
115112, 1143anbi13d 1437 . . 3 (𝑣 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) β†’ ((((𝐹 β†Ύ 𝐢) + 𝑣) = 𝐹 ∧ dom (𝐹 β†Ύ 𝐢) = 𝐢 ∧ dom 𝑣 = 𝐷) ↔ (((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = 𝐹 ∧ dom (𝐹 β†Ύ 𝐢) = 𝐢 ∧ dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = 𝐷)))
116110, 115rspc2ev 3625 . 2 (((𝐹 β†Ύ 𝐢) ∈ (ran 𝐹 ↑m 𝐢) ∧ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) ∈ (ran 𝐹 ↑m 𝐷) ∧ (((𝐹 β†Ύ 𝐢) + (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑)))) = 𝐹 ∧ dom (𝐹 β†Ύ 𝐢) = 𝐢 ∧ dom (𝑑 ∈ 𝐷 ↦ (πΉβ€˜(𝐢 +o 𝑑))) = 𝐷)) β†’ βˆƒπ‘’ ∈ (ran 𝐹 ↑m 𝐢)βˆƒπ‘£ ∈ (ran 𝐹 ↑m 𝐷)((𝑒 + 𝑣) = 𝐹 ∧ dom 𝑒 = 𝐢 ∧ dom 𝑣 = 𝐷))
11718, 29, 98, 103, 105, 116syl113anc 1381 1 ((𝐹 Fn (𝐢 +o 𝐷) ∧ (𝐢 ∈ On ∧ 𝐷 ∈ On)) β†’ βˆƒπ‘’ ∈ (ran 𝐹 ↑m 𝐢)βˆƒπ‘£ ∈ (ran 𝐹 ↑m 𝐷)((𝑒 + 𝑣) = 𝐹 ∧ dom 𝑒 = 𝐢 ∧ dom 𝑣 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βˆƒwrex 3069  Vcvv 3473   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949   class class class wbr 5149  {copab 5211   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β†Ύ cres 5679  Ord word 6364  Oncon0 6365  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7412   ∈ cmpo 7414   +o coa 8466   ↑m cmap 8823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-oadd 8473  df-map 8825
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator