Theorem ofoaf 44034

Description: Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.)

Assertion

Ref	Expression
ofoaf	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f +o ↾ ((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶))

Proof of Theorem ofoaf

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . . 4 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐸 = (ω ↑o 𝐷))
2		omelon 9618	. . . . 5 ⊢ ω ∈ On
3		simpl 487	. . . . 5 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐷 ∈ On)
4		oecl 8525	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐷 ∈ On) → (ω ↑o 𝐷) ∈ On)
5	2, 3, 4	sylancr 598	. . . 4 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → (ω ↑o 𝐷) ∈ On)
6	1, 5	eqeltrd 2870	. . 3 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐸 ∈ On)
7	3, 2	jctil 528	. . . . . . . 8 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → (ω ∈ On ∧ 𝐷 ∈ On))
8		peano1 7888	. . . . . . . 8 ⊢ ∅ ∈ ω
9		oen0 8575	. . . . . . . 8 ⊢ (((ω ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ ω) → ∅ ∈ (ω ↑o 𝐷))
10	7, 8, 9	sylancl 597	. . . . . . 7 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → ∅ ∈ (ω ↑o 𝐷))
11	10, 1	eleqtrrd 2873	. . . . . 6 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → ∅ ∈ 𝐸)
12		oveq1 7421	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 +o 𝐸) = (∅ +o 𝐸))
13	12	sseq2d 3977	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝐸 ⊆ (𝑥 +o 𝐸) ↔ 𝐸 ⊆ (∅ +o 𝐸)))
14	13	adantl 486	. . . . . 6 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 = ∅) → (𝐸 ⊆ (𝑥 +o 𝐸) ↔ 𝐸 ⊆ (∅ +o 𝐸)))
15		oa0r 8526	. . . . . . . 8 ⊢ (𝐸 ∈ On → (∅ +o 𝐸) = 𝐸)
16	6, 15	syl 18	. . . . . . 7 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → (∅ +o 𝐸) = 𝐸)
17		ssid 3967	. . . . . . 7 ⊢ (∅ +o 𝐸) ⊆ (∅ +o 𝐸)
18	16, 17	eqsstrrdi 3990	. . . . . 6 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐸 ⊆ (∅ +o 𝐸))
19	11, 14, 18	rspcedvd 3591	. . . . 5 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → ∃𝑥 ∈ 𝐸 𝐸 ⊆ (𝑥 +o 𝐸))
20		ssiun 5016	. . . . 5 ⊢ (∃𝑥 ∈ 𝐸 𝐸 ⊆ (𝑥 +o 𝐸) → 𝐸 ⊆ ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))
21	19, 20	syl 18	. . . 4 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐸 ⊆ ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))
22	1	eleq2d 2856	. . . . . . . 8 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ (ω ↑o 𝐷)))
23	22	biimpa 481	. . . . . . 7 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝑥 ∈ (ω ↑o 𝐷))
24	6	adantr 485	. . . . . . 7 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝐸 ∈ On)
25	1	adantr 485	. . . . . . . 8 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝐸 = (ω ↑o 𝐷))
26		ssid 3967	. . . . . . . 8 ⊢ 𝐸 ⊆ 𝐸
27	25, 26	eqsstrrdi 3990	. . . . . . 7 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → (ω ↑o 𝐷) ⊆ 𝐸)
28		oaabs2 8638	. . . . . . 7 ⊢ (((𝑥 ∈ (ω ↑o 𝐷) ∧ 𝐸 ∈ On) ∧ (ω ↑o 𝐷) ⊆ 𝐸) → (𝑥 +o 𝐸) = 𝐸)
29	23, 24, 27, 28	syl21anc 850	. . . . . 6 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → (𝑥 +o 𝐸) = 𝐸)
30	29, 26	eqsstrdi 3989	. . . . 5 ⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) ∧ 𝑥 ∈ 𝐸) → (𝑥 +o 𝐸) ⊆ 𝐸)
31	30	iunssd 5020	. . . 4 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸) ⊆ 𝐸)
32	21, 31	eqssd 3962	. . 3 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))
33	6, 6, 32	3jca 1144	. 2 ⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷)) → (𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸)))
34		ofoafg 44033	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))) → ( ∘f +o ↾ ((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶))
35	33, 34	sylan2 604	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f +o ↾ ((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2150  ∃wrex 3096   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  ∪ ciun 4961   × cxp 5663   ↾ cres 5667  Oncon0 6364  ⟶wf 6536  (class class class)co 7414   ∘_f cof 7676  ωcom 7865   +_o coa 8453   ↑_o coe 8455   ↑_m cmap 8827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5340  ax-pr 5408  ax-un 7736  ax-inf2 9613

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3464  df-sbc 3753  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5560  df-eprel 5565  df-po 5573  df-so 5574  df-fr 5618  df-we 5620  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7678  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-2o 8457  df-oadd 8460  df-omul 8461  df-oexp 8462  df-map 8829

This theorem is referenced by:  ofoafo  44035  ofoacl  44036