ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  enq0sym GIF version

Theorem enq0sym 7430
Description: The equivalence relation for nonnegative fractions is symmetric. Lemma for enq0er 7433. (Contributed by Jim Kingdon, 14-Nov-2019.)
Assertion
Ref Expression
enq0sym (๐‘“ ~Q0 ๐‘” โ†’ ๐‘” ~Q0 ๐‘“)

Proof of Theorem enq0sym
Dummy variables ๐‘Ž ๐‘ ๐‘ ๐‘‘ ๐‘ข ๐‘ฃ ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2740 . . . . . . . 8 ๐‘“ โˆˆ V
2 vex 2740 . . . . . . . 8 ๐‘” โˆˆ V
3 eleq1 2240 . . . . . . . . . 10 (๐‘ฅ = ๐‘“ โ†’ (๐‘ฅ โˆˆ (ฯ‰ ร— N) โ†” ๐‘“ โˆˆ (ฯ‰ ร— N)))
43anbi1d 465 . . . . . . . . 9 (๐‘ฅ = ๐‘“ โ†’ ((๐‘ฅ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โ†” (๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N))))
5 eqeq1 2184 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘“ โ†’ (๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โ†” ๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ))
65anbi1d 465 . . . . . . . . . . 11 (๐‘ฅ = ๐‘“ โ†’ ((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
76anbi1d 465 . . . . . . . . . 10 (๐‘ฅ = ๐‘“ โ†’ (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
874exbidv 1870 . . . . . . . . 9 (๐‘ฅ = ๐‘“ โ†’ (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
94, 8anbi12d 473 . . . . . . . 8 (๐‘ฅ = ๐‘“ โ†’ (((๐‘ฅ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)))))
10 eleq1 2240 . . . . . . . . . 10 (๐‘ฆ = ๐‘” โ†’ (๐‘ฆ โˆˆ (ฯ‰ ร— N) โ†” ๐‘” โˆˆ (ฯ‰ ร— N)))
1110anbi2d 464 . . . . . . . . 9 (๐‘ฆ = ๐‘” โ†’ ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โ†” (๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N))))
12 eqeq1 2184 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘” โ†’ (๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ โ†” ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ))
1312anbi2d 464 . . . . . . . . . . 11 (๐‘ฆ = ๐‘” โ†’ ((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
1413anbi1d 465 . . . . . . . . . 10 (๐‘ฆ = ๐‘” โ†’ (((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
15144exbidv 1870 . . . . . . . . 9 (๐‘ฆ = ๐‘” โ†’ (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
1611, 15anbi12d 473 . . . . . . . 8 (๐‘ฆ = ๐‘” โ†’ (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)))))
17 df-enq0 7422 . . . . . . . 8 ~Q0 = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)))}
181, 2, 9, 16, 17brab 4272 . . . . . . 7 (๐‘“ ~Q0 ๐‘” โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
1918biimpi 120 . . . . . 6 (๐‘“ ~Q0 ๐‘” โ†’ ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
20 opeq12 3780 . . . . . . . . . . 11 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ = โŸจ๐‘Ž, ๐‘โŸฉ)
2120eqeq2d 2189 . . . . . . . . . 10 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ (๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โ†” ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ))
2221anbi1d 465 . . . . . . . . 9 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ ((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
23 simpl 109 . . . . . . . . . . 11 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ ๐‘ง = ๐‘Ž)
2423oveq1d 5889 . . . . . . . . . 10 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ (๐‘ง ยทo ๐‘ข) = (๐‘Ž ยทo ๐‘ข))
25 simpr 110 . . . . . . . . . . 11 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ ๐‘ค = ๐‘)
2625oveq1d 5889 . . . . . . . . . 10 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ (๐‘ค ยทo ๐‘ฃ) = (๐‘ ยทo ๐‘ฃ))
2724, 26eqeq12d 2192 . . . . . . . . 9 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ ((๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ) โ†” (๐‘Ž ยทo ๐‘ข) = (๐‘ ยทo ๐‘ฃ)))
2822, 27anbi12d 473 . . . . . . . 8 ((๐‘ง = ๐‘Ž โˆง ๐‘ค = ๐‘) โ†’ (((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘Ž ยทo ๐‘ข) = (๐‘ ยทo ๐‘ฃ))))
29 opeq12 3780 . . . . . . . . . . 11 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ โŸจ๐‘ฃ, ๐‘ขโŸฉ = โŸจ๐‘, ๐‘‘โŸฉ)
3029eqeq2d 2189 . . . . . . . . . 10 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ (๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ โ†” ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ))
3130anbi2d 464 . . . . . . . . 9 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ)))
32 simpr 110 . . . . . . . . . . 11 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ ๐‘ข = ๐‘‘)
3332oveq2d 5890 . . . . . . . . . 10 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ (๐‘Ž ยทo ๐‘ข) = (๐‘Ž ยทo ๐‘‘))
34 simpl 109 . . . . . . . . . . 11 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ ๐‘ฃ = ๐‘)
3534oveq2d 5890 . . . . . . . . . 10 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ (๐‘ ยทo ๐‘ฃ) = (๐‘ ยทo ๐‘))
3633, 35eqeq12d 2192 . . . . . . . . 9 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ ((๐‘Ž ยทo ๐‘ข) = (๐‘ ยทo ๐‘ฃ) โ†” (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘)))
3731, 36anbi12d 473 . . . . . . . 8 ((๐‘ฃ = ๐‘ โˆง ๐‘ข = ๐‘‘) โ†’ (((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘Ž ยทo ๐‘ข) = (๐‘ ยทo ๐‘ฃ)) โ†” ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
3828, 37cbvex4v 1930 . . . . . . 7 (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘)))
3938anbi2i 457 . . . . . 6 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘“ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘” = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
4019, 39sylib 122 . . . . 5 (๐‘“ ~Q0 ๐‘” โ†’ ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
41 19.42vv 1911 . . . . 5 (โˆƒ๐‘Žโˆƒ๐‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
4240, 41sylibr 134 . . . 4 (๐‘“ ~Q0 ๐‘” โ†’ โˆƒ๐‘Žโˆƒ๐‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
43 19.42vv 1911 . . . . 5 (โˆƒ๐‘โˆƒ๐‘‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†” ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
44432exbii 1606 . . . 4 (โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†” โˆƒ๐‘Žโˆƒ๐‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
4542, 44sylibr 134 . . 3 (๐‘“ ~Q0 ๐‘” โ†’ โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))))
46 pm3.22 265 . . . . . . 7 ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โ†’ (๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)))
4746adantr 276 . . . . . 6 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ (๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)))
48 pm3.22 265 . . . . . . 7 ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โ†’ (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ))
4948ad2antrl 490 . . . . . 6 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ))
50 simprr 531 . . . . . . . 8 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))
51 eleq1 2240 . . . . . . . . . . . . . 14 (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘“ โˆˆ (ฯ‰ ร— N) โ†” โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ (ฯ‰ ร— N)))
52 opelxp 4656 . . . . . . . . . . . . . 14 (โŸจ๐‘Ž, ๐‘โŸฉ โˆˆ (ฯ‰ ร— N) โ†” (๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N))
5351, 52bitrdi 196 . . . . . . . . . . . . 13 (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘“ โˆˆ (ฯ‰ ร— N) โ†” (๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N)))
5453biimpcd 159 . . . . . . . . . . . 12 (๐‘“ โˆˆ (ฯ‰ ร— N) โ†’ (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โ†’ (๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N)))
55 eleq1 2240 . . . . . . . . . . . . . 14 (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โ†’ (๐‘” โˆˆ (ฯ‰ ร— N) โ†” โŸจ๐‘, ๐‘‘โŸฉ โˆˆ (ฯ‰ ร— N)))
56 opelxp 4656 . . . . . . . . . . . . . 14 (โŸจ๐‘, ๐‘‘โŸฉ โˆˆ (ฯ‰ ร— N) โ†” (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N))
5755, 56bitrdi 196 . . . . . . . . . . . . 13 (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โ†’ (๐‘” โˆˆ (ฯ‰ ร— N) โ†” (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N)))
5857biimpcd 159 . . . . . . . . . . . 12 (๐‘” โˆˆ (ฯ‰ ร— N) โ†’ (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โ†’ (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N)))
5954, 58im2anan9 598 . . . . . . . . . . 11 ((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โ†’ ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โ†’ ((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N) โˆง (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N))))
6059imp 124 . . . . . . . . . 10 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง (๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ)) โ†’ ((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N) โˆง (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N)))
6160adantrr 479 . . . . . . . . 9 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ ((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N) โˆง (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N)))
62 pinn 7307 . . . . . . . . . . . 12 (๐‘‘ โˆˆ N โ†’ ๐‘‘ โˆˆ ฯ‰)
63 nnmcom 6489 . . . . . . . . . . . 12 ((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ ฯ‰) โ†’ (๐‘Ž ยทo ๐‘‘) = (๐‘‘ ยทo ๐‘Ž))
6462, 63sylan2 286 . . . . . . . . . . 11 ((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N) โ†’ (๐‘Ž ยทo ๐‘‘) = (๐‘‘ ยทo ๐‘Ž))
65 pinn 7307 . . . . . . . . . . . 12 (๐‘ โˆˆ N โ†’ ๐‘ โˆˆ ฯ‰)
66 nnmcom 6489 . . . . . . . . . . . 12 ((๐‘ โˆˆ ฯ‰ โˆง ๐‘ โˆˆ ฯ‰) โ†’ (๐‘ ยทo ๐‘) = (๐‘ ยทo ๐‘))
6765, 66sylan 283 . . . . . . . . . . 11 ((๐‘ โˆˆ N โˆง ๐‘ โˆˆ ฯ‰) โ†’ (๐‘ ยทo ๐‘) = (๐‘ ยทo ๐‘))
6864, 67eqeqan12d 2193 . . . . . . . . . 10 (((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N) โˆง (๐‘ โˆˆ N โˆง ๐‘ โˆˆ ฯ‰)) โ†’ ((๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘) โ†” (๐‘‘ ยทo ๐‘Ž) = (๐‘ ยทo ๐‘)))
6968an42s 589 . . . . . . . . 9 (((๐‘Ž โˆˆ ฯ‰ โˆง ๐‘ โˆˆ N) โˆง (๐‘ โˆˆ ฯ‰ โˆง ๐‘‘ โˆˆ N)) โ†’ ((๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘) โ†” (๐‘‘ ยทo ๐‘Ž) = (๐‘ ยทo ๐‘)))
7061, 69syl 14 . . . . . . . 8 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ ((๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘) โ†” (๐‘‘ ยทo ๐‘Ž) = (๐‘ ยทo ๐‘)))
7150, 70mpbid 147 . . . . . . 7 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ (๐‘‘ ยทo ๐‘Ž) = (๐‘ ยทo ๐‘))
7271eqcomd 2183 . . . . . 6 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))
7347, 49, 72jca32 310 . . . . 5 (((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
74732eximi 1601 . . . 4 (โˆƒ๐‘โˆƒ๐‘‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
75742eximi 1601 . . 3 (โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘“ โˆˆ (ฯ‰ ร— N) โˆง ๐‘” โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ) โˆง (๐‘Ž ยทo ๐‘‘) = (๐‘ ยทo ๐‘))) โ†’ โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
7645, 75syl 14 . 2 (๐‘“ ~Q0 ๐‘” โ†’ โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
77 exrot4 1691 . . 3 (โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†” โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
78 19.42vv 1911 . . . . 5 (โˆƒ๐‘Žโˆƒ๐‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†” ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
79782exbii 1606 . . . 4 (โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†” โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
80 19.42vv 1911 . . . . 5 (โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†” ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
81 opeq12 3780 . . . . . . . . . 10 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ โŸจ๐‘ง, ๐‘คโŸฉ = โŸจ๐‘, ๐‘‘โŸฉ)
8281eqeq2d 2189 . . . . . . . . 9 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ (๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โ†” ๐‘” = โŸจ๐‘, ๐‘‘โŸฉ))
8382anbi1d 465 . . . . . . . 8 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ ((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
84 simpl 109 . . . . . . . . . 10 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ ๐‘ง = ๐‘)
8584oveq1d 5889 . . . . . . . . 9 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ (๐‘ง ยทo ๐‘ข) = (๐‘ ยทo ๐‘ข))
86 simpr 110 . . . . . . . . . 10 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ ๐‘ค = ๐‘‘)
8786oveq1d 5889 . . . . . . . . 9 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ (๐‘ค ยทo ๐‘ฃ) = (๐‘‘ ยทo ๐‘ฃ))
8885, 87eqeq12d 2192 . . . . . . . 8 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ ((๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ) โ†” (๐‘ ยทo ๐‘ข) = (๐‘‘ ยทo ๐‘ฃ)))
8983, 88anbi12d 473 . . . . . . 7 ((๐‘ง = ๐‘ โˆง ๐‘ค = ๐‘‘) โ†’ (((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ ยทo ๐‘ข) = (๐‘‘ ยทo ๐‘ฃ))))
90 opeq12 3780 . . . . . . . . . 10 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ โŸจ๐‘ฃ, ๐‘ขโŸฉ = โŸจ๐‘Ž, ๐‘โŸฉ)
9190eqeq2d 2189 . . . . . . . . 9 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ (๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ โ†” ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ))
9291anbi2d 464 . . . . . . . 8 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ)))
93 simpr 110 . . . . . . . . . 10 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ ๐‘ข = ๐‘)
9493oveq2d 5890 . . . . . . . . 9 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ (๐‘ ยทo ๐‘ข) = (๐‘ ยทo ๐‘))
95 simpl 109 . . . . . . . . . 10 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ ๐‘ฃ = ๐‘Ž)
9695oveq2d 5890 . . . . . . . . 9 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ (๐‘‘ ยทo ๐‘ฃ) = (๐‘‘ ยทo ๐‘Ž))
9794, 96eqeq12d 2192 . . . . . . . 8 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ ((๐‘ ยทo ๐‘ข) = (๐‘‘ ยทo ๐‘ฃ) โ†” (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž)))
9892, 97anbi12d 473 . . . . . . 7 ((๐‘ฃ = ๐‘Ž โˆง ๐‘ข = ๐‘) โ†’ (((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ ยทo ๐‘ข) = (๐‘‘ ยทo ๐‘ฃ)) โ†” ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))))
9989, 98cbvex4v 1930 . . . . . 6 (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž)))
100 eleq1 2240 . . . . . . . . . 10 (๐‘ฅ = ๐‘” โ†’ (๐‘ฅ โˆˆ (ฯ‰ ร— N) โ†” ๐‘” โˆˆ (ฯ‰ ร— N)))
101100anbi1d 465 . . . . . . . . 9 (๐‘ฅ = ๐‘” โ†’ ((๐‘ฅ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โ†” (๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N))))
102 eqeq1 2184 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘” โ†’ (๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โ†” ๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ))
103102anbi1d 465 . . . . . . . . . . 11 (๐‘ฅ = ๐‘” โ†’ ((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
104103anbi1d 465 . . . . . . . . . 10 (๐‘ฅ = ๐‘” โ†’ (((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
1051044exbidv 1870 . . . . . . . . 9 (๐‘ฅ = ๐‘” โ†’ (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
106101, 105anbi12d 473 . . . . . . . 8 (๐‘ฅ = ๐‘” โ†’ (((๐‘ฅ โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘ฅ = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†” ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)))))
107 eleq1 2240 . . . . . . . . . 10 (๐‘ฆ = ๐‘“ โ†’ (๐‘ฆ โˆˆ (ฯ‰ ร— N) โ†” ๐‘“ โˆˆ (ฯ‰ ร— N)))
108107anbi2d 464 . . . . . . . . 9 (๐‘ฆ = ๐‘“ โ†’ ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โ†” (๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N))))
109 eqeq1 2184 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘“ โ†’ (๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ โ†” ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ))
110109anbi2d 464 . . . . . . . . . . 11 (๐‘ฆ = ๐‘“ โ†’ ((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โ†” (๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ)))
111110anbi1d 465 . . . . . . . . . 10 (๐‘ฆ = ๐‘“ โ†’ (((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” ((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
1121114exbidv 1870 . . . . . . . . 9 (๐‘ฆ = ๐‘“ โ†’ (โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)) โ†” โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
113108, 112anbi12d 473 . . . . . . . 8 (๐‘ฆ = ๐‘“ โ†’ (((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘ฆ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘ฆ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†” ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ)))))
1142, 1, 106, 113, 17brab 4272 . . . . . . 7 (๐‘” ~Q0 ๐‘“ โ†” ((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))))
115114biimpri 133 . . . . . 6 (((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘งโˆƒ๐‘คโˆƒ๐‘ฃโˆƒ๐‘ข((๐‘” = โŸจ๐‘ง, ๐‘คโŸฉ โˆง ๐‘“ = โŸจ๐‘ฃ, ๐‘ขโŸฉ) โˆง (๐‘ง ยทo ๐‘ข) = (๐‘ค ยทo ๐‘ฃ))) โ†’ ๐‘” ~Q0 ๐‘“)
11699, 115sylan2br 288 . . . . 5 (((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†’ ๐‘” ~Q0 ๐‘“)
11780, 116sylbi 121 . . . 4 (โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง โˆƒ๐‘Žโˆƒ๐‘((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†’ ๐‘” ~Q0 ๐‘“)
11879, 117sylbi 121 . . 3 (โˆƒ๐‘โˆƒ๐‘‘โˆƒ๐‘Žโˆƒ๐‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†’ ๐‘” ~Q0 ๐‘“)
11977, 118sylbi 121 . 2 (โˆƒ๐‘Žโˆƒ๐‘โˆƒ๐‘โˆƒ๐‘‘((๐‘” โˆˆ (ฯ‰ ร— N) โˆง ๐‘“ โˆˆ (ฯ‰ ร— N)) โˆง ((๐‘” = โŸจ๐‘, ๐‘‘โŸฉ โˆง ๐‘“ = โŸจ๐‘Ž, ๐‘โŸฉ) โˆง (๐‘ ยทo ๐‘) = (๐‘‘ ยทo ๐‘Ž))) โ†’ ๐‘” ~Q0 ๐‘“)
12076, 119syl 14 1 (๐‘“ ~Q0 ๐‘” โ†’ ๐‘” ~Q0 ๐‘“)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148  โŸจcop 3595   class class class wbr 4003  ฯ‰com 4589   ร— cxp 4624  (class class class)co 5874   ยทo comu 6414  Ncnpi 7270   ~Q0 ceq0 7284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-oadd 6420  df-omul 6421  df-ni 7302  df-enq0 7422
This theorem is referenced by:  enq0er  7433
  Copyright terms: Public domain W3C validator